What is G4ip ?

G4ip is the name of the sequent system for intuitionistic propositional logic invented by Roy Dyckhoff.

I have implemented G4ip in a Prolog file that I have called G4ip.pl. This program is only a modification of seqprover.pl, a sequent calculus prover written by Naoyuki Tamura, available at this address:

[[ http://bach.istc.kobe-u.ac.jp/seqprover/ ]]

I put my G4ip.pl on Github to share and to improve my work.

TODO LIST

matching this program with bussproofs.sty to make sequent proofs in LaTeX form. (seqprover.pl do it with proof.sty, therefore I guess that G4ip.pl cand do it also with proof.sty ; I wonder if one can use bussproofs.sty that I prefer.)

writing a prover for intuitionistic first order logic, and not only propositional logic.