10 ms·

Oh, that paper is very interesting, thanks for that. It's not really comparable to a fully formal system, though: The user essentially chooses which trivial thi

Oh, that paper is very interesting, thanks for that. It's not really comparable to a fully formal system, though: The user essentially chooses which trivial things to prove to convince themselves of something. For example, a real proof assistant would tell you what exactly to prove for the inductive proof in the factorial example. In this system you pick an induction principle yourself and hope it's correct. Still, I'd like to see more work along these lines.

carapace 7y ago
It's Prolog, so there is probably already more. I just found a bachelor thesis from 2011 "Implementation of a Proof Assistant in Prolog" https://www2.imm.dtu.dk/pubdb/views/edoc_download.php/6043/pdf/imm6043.pdf https://www2.imm.dtu.dk/pubdb/views/edoc_download.php/6043/p... I haven't read it yet. There's also PRESS, which seems relevant, "Solving symbolic equations with PRESS" > We describe a program, PRESS, (PRolog Equation Solving System) for solving symbolic, transcendental, non-differential equations in one or more variables. PRESS solves autonomously, i.e. without guidance from the user. The methods used for solving equations are described, together with the service facilities. The principal technique, meta-level inference, appears to be relevant to the broader field of symbolic and algebraic manipulation. https://www.sciencedirect.com/science/article/pii/S0747717189800070 https://www.sciencedirect.com/science/article/pii/S074771718... https://github.com/maths/press https://github.com/maths/press I'm not trying to promote Prolog over TLA+ or anything, I've only just started with TLA+.