# LaTeX proofs via seqprover.pl (a SWI-Prolog logical theorem prover ) **URL:** \ **Category:** Nice to know\ **Tags:** how-to\ **Created:** [January 14, 2022, 9:35am UTC](https://swi-prolog.discourse.group/t/latex-proofs-via-seqprover-pl-a-swi-prolog-logical-theorem-prover/4895 "2022-01-14T09:35:56Z")\ **Posts on this page:** 5\ **Page:** 1
**Author:** ![joseph-vidal-rosset](https://yyz2.discourse-cdn.com/free1/user_avatar/swi-prolog.discourse.group/joseph-vidal-rosset/32/2594_2.png) [@joseph-vidal-rosset](https://swi-prolog.discourse.group/u/joseph-vidal-rosset)\ **Post date:** [January 14, 2022, 9:35am UTC](https://swi-prolog.discourse.group/t/latex-proofs-via-seqprover-pl-a-swi-prolog-logical-theorem-prover/4895/1 "2022-01-14T09:35:56Z")
[seqprover.pl](https://gitlab.com/cspsat/seqprover-gitpod/-/blob/master/seqprover.pl) is a very nice SWI-Prolog sequent prover in Classical First-Order Logic made by [Naoyuki Tamura.](https://www.researchgate.net/profile/Naoyuki-Tamura). This prover can provides proofs in LaTeX via proof.sty . I published [a fork of seqprover.pl](https://www.vidal-rosset.net/g4-prover/) 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: ![proof](https://global.discourse-cdn.com/free1/uploads/swiprolog/original/2X/1/174c3dbb75207a85508f9dd3a0dc13ef14e03a24.jpeg) Unfortunately, proof.sty is not in MathJax. ---
**Author:** ![joseph-vidal-rosset](https://yyz2.discourse-cdn.com/free1/user_avatar/swi-prolog.discourse.group/joseph-vidal-rosset/32/2594_2.png) [@joseph-vidal-rosset](https://swi-prolog.discourse.group/u/joseph-vidal-rosset)\ **Post date:** [January 14, 2022, 10:15am UTC](https://swi-prolog.discourse.group/t/latex-proofs-via-seqprover-pl-a-swi-prolog-logical-theorem-prover/4895/3 "2022-01-14T10:15:56Z")
> [@anon95304481](#): > > Sorry no (\<=\>)/2 yet. A simple proof only needs 2 contractions > of some quantifers that are subject to contraction. I added (\<=\>/2) and indeed, this prover provides the proof in a blink: ```prolog ?- | 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. ---
**Author:** ![joseph-vidal-rosset](https://yyz2.discourse-cdn.com/free1/user_avatar/swi-prolog.discourse.group/joseph-vidal-rosset/32/2594_2.png) [@joseph-vidal-rosset](https://swi-prolog.discourse.group/u/joseph-vidal-rosset)\ **Post date:** [January 14, 2022, 10:25am UTC](https://swi-prolog.discourse.group/t/latex-proofs-via-seqprover-pl-a-swi-prolog-logical-theorem-prover/4895/4 "2022-01-14T10:25:06Z")
> [@anon95304481](#): > > Jens Ottens prover leanseq\_v5.pl is possibly superior for classical > logic. The website with Naoyuki Tamuras prover says: 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 : ```prolog 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 = ``` ---
**Author:** ![mgondan1](https://yyz2.discourse-cdn.com/free1/user_avatar/swi-prolog.discourse.group/mgondan1/32/803_2.png) [@mgondan1](https://swi-prolog.discourse.group/u/mgondan1)\ **Post date:** [January 16, 2022, 10:12am UTC](https://swi-prolog.discourse.group/t/latex-proofs-via-seqprover-pl-a-swi-prolog-logical-theorem-prover/4895/7 "2022-01-16T10:12:39Z")
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 ```prolog 2x ``` ---
**Author:** ![mgondan1](https://yyz2.discourse-cdn.com/free1/user_avatar/swi-prolog.discourse.group/mgondan1/32/803_2.png) [@mgondan1](https://swi-prolog.discourse.group/u/mgondan1)\ **Post date:** [January 16, 2022, 12:09pm UTC](https://swi-prolog.discourse.group/t/latex-proofs-via-seqprover-pl-a-swi-prolog-logical-theorem-prover/4895/9 "2022-01-16T12:09:59Z")
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).