Sequent Prover (seqprover) A sequent prover for classical first order logic

, par Naoyuki Tamura

This small program seqprover.pl (written in SICStus Prolog and running into this website thanks to SWI-Prolog) searches a cut-free proof of the given sequent of first-order logic. Of course, the proof search of first-order logic is undecidable. Therefore, this program limits the number of quantifier rules (L\forall and R\exists) for each path of the proof at most five. To format LaTeX output, you need proof.sty by Makoto Tatsuta, and please add the following lines to your LaTeX source file.

\newcommand{\imp}{\supset}
\newcommand{\lra}{\longrightarrow}

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 .

Voir en ligne : The original seqprover webpage

P.-S.

Many thanks to François Elie who wrote the PHP code for this prover in this website.

Any comments or suggestions are appreciated (tamura @ kobe-u.ac.jp).