In Memoriam Roy Dyckhoff

G4 Prover A sequent calculus prover with G4 rules

, par Joseph Vidal-Rosset

This prover is a fork that I developed from seqprover.pl that is Naoyuki Tamura’s prover for sequent calculus CL-X.
I am a lot indebted to Naoyuki Tamura’s work, because I needed to change almost only the logical rules of his program to succeed in writing this prover that provides proof in sequent calculus G4. The logical rules of this program are the rules that was defined by Dyckhoff [1] and by Dyckhoff and Negri [2]. Thanks to the clarity of Naoyuki Tamura’s Prolog code, their implementation in this prover was an easy task.
The syntax of this prover is the same that Naoyuki Tamura’s prover.
To format LaTeX output, you need proof.sty by Makoto Tatsuta.
Note that :
a - Occur check is not included.
b - Do not use free variables, i.e. the following code : a(X) --> a(1) is unsound.
c - The disjunction symbol is not the letter v but \/.
d - The conjunction symbol is /\.
e - Do not confuse the derivation symbol --> used to express sequents, with the conditional symbol -> .
f - Last, it is obligatory to input sequents. It means that, to test the theoremhood of formula F, the input must be top --> F .

Notes

[1 Dyckhoff R. Contraction-free sequent calculi for intuitionistic logic. Journal of Symbolic Logic. 1992;57(3):795-807. Available at: http://www.jstor.org/stable/2275431?origin=JSTOR-pdf. Consulté sans date.

[2 Dyckhoff R, Negri S. Admissibility of Structural Rules for Contraction-Free Systems of Intuitionistic Logic. Journal of Symbolic Logic. 2000.