Sequent Prover (seqprover)

What's New

Dec 30, 2020: GitPod for running seqprover
- See https://gitlab.com/cspsat/seqprover-gitpod
Dec 19, 2020: Version 2.0
- Modified for SWI Prolog
Dec 15, 2020: Move to new site (https://cspsat.gitlab.io/seqprover/)

Introduction

This small program seqprover.pl (written in 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}

Documents

Please refer to guide.pdf for notations and inference rules.

Known Bugs

Occur check is not included.
Do not use free variables (e.g. a(X) --> a(1)).
"X@Y@p --> p" cannot be proved (reported by Joseph Vidal-Rosset on July 15, 2019)

Joseph Vidal-Rosset's prover

g4-prover.pl by Joseph Vidal-Rosset is a prover in minimal FOL, intuitionistic FOL and classical FOL in G4 sequent calculus.