seqprover.pl is a very nice SWI-Prolog sequent prover in Classical First-Order Logic made by Naoyuki Tamura. . This prover can provides proofs in LaTeX via proof.sty . I published a fork of seqprover.pl for G4ip sequent system. Note that the LaTeX proofs provided by this prover are very clean, even for the predicate calculus. See the following image of this sequent proof:
Unfortunately, proof.sty is not in MathJax.
I added (<=>/2) and indeed, this prover provides the proof in a blink:
?- | provable(((~(?[X]:(p(X)&q(X))))<=>(![X]:(p(X)=> ~ q(X)))), Proof).
% 26,942 inferences, 0.009 CPU in 0.009 seconds (100% CPU, 3010086 Lips)
Prolog output : rbicond([]>[(~ ?[_18]:(p(_18)&q(_18))<=>![_18]:(p(_18)=> ~q(_18)))],lneg([~ ?[_18]:(p(_18)&q(_18))]>[![_18]:(p(_18)=> ~q(_18))],rforall([]>[?[_18]:(p(_18)&q(_18)),![_18]:(p(_18)=> ~q(_18))],rcond([]>[(p(f_sk(1,[]))=> ~q(f_sk(1,[]))),?[_18]:(p(_18)&q(_18))],rneg([p(f_sk(1,[]))]>[~q(f_sk(1,[])),?[_18]:(p(_18)&q(_18))],rexists([q(f_sk(1,[])),p(f_sk(1,[]))]>[?[_18]:(p(_18)&q(_18))],rand([q(f_sk(1,[])),p(f_sk(1,[]))]>[(p(f_sk(1,[]))&q(f_sk(1,[]))),?[_18]:(p(_18)&q(_18))],ax([q(f_sk(1,[])),p(f_sk(1,[]))]>[p(f_sk(1,[])),?[_18]:(p(_18)&q(_18))],ax),ax([q(f_sk(1,[])),p(f_sk(1,[]))]>[q(f_sk(1,[])),?[_18]:(p(_18)&q(_18))],ax))))))),rneg([![_18]:(p(_18)=> ~q(_18))]>[~ ?[_18]:(p(_18)&q(_18))],lexists([?[_18]:(p(_18)&q(_18)),![_18]:(p(_18)=> ~q(_18))]>[],land([(p(f_sk(2,[]))&q(f_sk(2,[]))),![_18]:(p(_18)=> ~q(_18))]>[],lforall([p(f_sk(2,[])),q(f_sk(2,[])),![_18]:(p(_18)=> ~q(_18))]>[],lcond([(p(f_sk(2,[]))=> ~q(f_sk(2,[]))),p(f_sk(2,[])),q(f_sk(2,[])),![_18]:(p(_18)=> ~q(_18))]>[],ax([p(f_sk(2,[])),q(f_sk(2,[])),![_18]:(p(_18)=> ~q(_18))]>[p(f_sk(2,[]))],ax),lneg([~q(f_sk(2,[])),p(f_sk(2,[])),q(f_sk(2,[])),![_18]:(p(_18)=> ~q(_18))]>[],ax([p(f_sk(2,[])),q(f_sk(2,[])),![_18]:(p(_18)=> ~q(_18))]>[q(f_sk(2,[]))],ax))))))))
Unfortunately, I did not succeed to write correctly the latex-pretty printer for FOL.
The slowness is more probably caused by the complexity of intuitionistic logic, in spite of G4i efficiency. Here is the result in classical logic with seqprover.pl :
Trying to prove with threshold = 0 1
Succeed in proving ~_6124#(p(_6124)/\q(_6124)) --> _6124@(p(_6124)-> ~q(_6124)) (2 msec.)
pretty:2 =
Trying to prove with threshold = 0 1
Succeed in proving _6124@(p(_6124)-> ~q(_6124)) --> ~_6124#(p(_6124)/\q(_6124)) (2 msec.)
pretty:3 =
Do you need some library that translates Prolog terms to some nice math representation? I have started such a thing for MathML, in case you’re interested. Things like
2^x
To
<msup><mn>2</mn><mi>x</mi></msup>
Maybe my example was not well chosen, since 2^x is meaningful in Prolog and Latex. The thing still is, how do we get from Prolog to Latex (or MathML if you prefer).