The Dogelog Runtime goes now by the name Dogelog Player. It is a Prolog interpreter which is written in 100% Prolog itself. Means it is based on a small native kernel, but most of it is written in Prolog itself, like clause compilation, clause indexing and term input/output.
To demonstrate some of its capabilities we made a series of experiments in rendering Jens Ottens Lean Prover proofs with the help of Dogelog Player. We started with propositional logic and walked our ways into first order logic. As a demo we can automatically render a proof of the Barber Paradox.
On a Cade19 tutorial website Jens Otten has published a couple of automated theorem provers written Prolog. They might be considered lean, since they do not require some difficult staging such as having files with the desired theorems, and then files with their conjunctive normal form. One can directly call a predicate prove0/1 in a Prolog top-level and experiment with different theorems.
The provers can be further considered lean since they don't demand much from the underlying Prolog system. A couple of the ISO core standard predicates such as unify_with_occurs_check/2 and copy_term/2 do the job. Lets look at a prenex normal form Q1x1…QnxnM, the provers mainly work according to the following principle:
- Qj=∀: is handled by a Skolem function.
- Qj=∃: is handled by fresh variable and contraction.
The FOL matrice M is then solved by unification and backtracking. Phil Zucker recently posted a website where he showed how to display a reduction tree in the propositional logic case. We took up the idea and extended it towards the first order logic case.
Build Your Own First-Order Prover | Tutorial at CADE 2019
Automated Propositional Sequent Proofs in Your Browser with Tau Prolog
TPTP Syntax without modification:
?- prove0((![X]:p(X) => ![Y]:(p(Y) & p(f(Y)))), 1).
TPTP Syntax with modification:
?- prove0((![X='x']:p(X) => ![Y='y']:(p(Y) & p(f(Y)))), 1).
Unlike Phil Zuckers take, we wrote the MathJax generation completely in Prolog itself using DCGs. We also saw to it that an LK calculus proof is extracted from the found reduction tree. LK calculus proofs are more readable, since they omit unnecessary formulas in the sequents:
Live demo available here:
Dogelog MathJax Herbrand
Although we were happy with our LK calculus MathJax rendering here, the latex itself is not very E-mail friendly. The commands are verbose and the markup is without numbering. So we explored the alternative of Unicode. We did this first in the browser but it also runs from within Python. The below shows a first order logic proof of the Barber Paradox.
Paradoxically there exists no Barber that shaves everybody s(x,y) that cannot shave himself ~s(y,y) and vice versa. The first order logic prover allows experimenting with other queries, like the formula from ex_barber.pl on Jens Ottens homepage. For running the Python version, we found choosing a certain font, like for example NSimSum, helps.
Live demo available here:
Dogelog Unicode List
We gave the end-user more control by a predicate prove0/2 where the second integer parameter gives the desired contraction depth. We could also provide an alternative output to MathJax by using the Unicode features of Dogelog Player. We can then even run the first order logic prover from within a Python interpreter using the Dogelog Player top-level.
Follow us on Twitter or Facebook:
Dogelog Twitter Account
Dogelog Facebook Account