Sequent Calculus Prover with Antisequents for Classical Propositional Logic

2021-12-16, updated 2021-12-16 next - previous

A prover developed from Zucker’s work, itself based on Jens Otten’s lectures.

This Prolog prover for classical propositional logic is an implementation of 12 rules which are the rules for the connectives in \(\mathbf{LK}\) [1 p. 187], and three additional rules: two rules (left and right) for the biconditional [2 p. 5], and an initial rule to prove falsifiability, which is the axiom of LK, a refutation system based on antisequents [3 p. 20].

Last, note, about the rules below, that the Weakening rules are built in the initial rule Ax., that there is no Contraction neither Cut, and that falsity constant \(\bot\) is not used in this system.

Initial rule for provability Initial rule for unprovability
\begin{prooftree} \AxiomC{}\RightLabel{\(\scriptsize{Ax.}\)}\UnaryInfC{$\Gamma, A \vdash A, \Delta$}\end{prooftree} \begin{prooftree} \AxiomC{}\RightLabel{\(\scriptsize{Asq.}\)}\UnaryInfC{$\Gamma \nvdash \Delta$}\noLine\UnaryInfC{$\Gamma \cap \Delta = \emptyset$}\end{prooftree}
Left rules Right rules
\begin{prooftree} \AxiomC{$\Gamma, A, B \vdash \Delta$}\RightLabel{\(\scriptsize{L\land}\)}\UnaryInfC{$\Gamma, A \land B \vdash \Delta$}\end{prooftree} \begin{prooftree}\AxiomC{$\Gamma \vdash A, \Delta$} \AxiomC{$\Gamma \vdash B, \Delta$}\RightLabel{\(\scriptsize{R\land}\)}\BinaryInfC{$\Gamma \vdash A \land B, \Delta$} \end{prooftree}
\begin{prooftree}\AxiomC{$\Gamma, A \vdash \Delta$} \AxiomC{$\Gamma, B \vdash \Delta$}\RightLabel{\(\scriptsize{L\lor}\)}\BinaryInfC{$\Gamma, A \lor B \vdash \Delta$} \end{prooftree} \begin{prooftree} \AxiomC{$\Gamma \vdash A, B, \Delta$}\RightLabel{\(\scriptsize{R\lor}\)}\UnaryInfC{$\Gamma \vdash A \lor B, \Delta$}\end{prooftree}
\begin{prooftree}\AxiomC{$\Gamma \vdash A, \Delta$} \AxiomC{$\Gamma, B \vdash \Delta$}\RightLabel{\(\scriptsize{L\to}\)}\BinaryInfC{$\Gamma, A \to B \vdash \Delta$} \end{prooftree} \begin{prooftree} \AxiomC{$\Gamma, A \vdash B, \Delta$}\RightLabel{\(\scriptsize{R\to}\)}\UnaryInfC{$\Gamma \vdash A \to B, \Delta$}\end{prooftree}
\begin{prooftree} \AxiomC{$\Gamma \vdash A, \Delta$}\RightLabel{\(\scriptsize{L\lnot}\)}\UnaryInfC{$\Gamma, \lnot A \vdash \Delta$}\end{prooftree} \begin{prooftree} \AxiomC{$\Gamma, A \vdash \Delta$}\RightLabel{\(\scriptsize{R\lnot}\)}\UnaryInfC{$\Gamma \vdash \lnot A, \Delta$}\end{prooftree}
\begin{prooftree}\AxiomC{$\Gamma, A, B \vdash \Delta$} \AxiomC{$\Gamma \vdash A, B, \Delta$}\RightLabel{\(\scriptsize{L\leftrightarrow}\)}\BinaryInfC{$\Gamma, A \leftrightarrow B \vdash \Delta$} \end{prooftree} \begin{prooftree}\AxiomC{$\Gamma, A \vdash B, \Delta$} \AxiomC{$\Gamma, B \vdash A, \Delta$}\RightLabel{\(\scriptsize{R\leftrightarrow}\)}\BinaryInfC{$\Gamma \vdash A \leftrightarrow B, \Delta$} \end{prooftree}

1. HOWTO

  • Select a query in section D- Examples of Queries, or write a Prolog query like:

    provable((your_formula), Proof).

    “your_formula” must a propositional formula respecting the syntax for the connectives given at the beginning of the Prolog file below.

  • If your formula is provable in classical propositional logic, all paths of the proof provided by the prover end on a sequent which is a logical axiom (label Ax.).
  • If your formula is unprovable in classical propositional logic, there is at least one path of the refutation provided by the prover which ends on one antisequent (label Asq, antisequents outputs are red), that is a sequent which is unprovable because no atomic formula occurs on both sides of the derivation symbol i.e. \(\vdash\). Note that each antisequent provides a countermodel. For example, formula 10 has two countermodels: \(\{A = true, B = false\}\) and \(\{A = false, B = true\}\). To the syntactical non-derivability expressed by \(A \nvdash B\) and \(B \nvdash A\) on which ends the refutation of \((A \lor B) \to (A \land B)\) provided by the prover, corresponds, by completeness, implications \(A \Rightarrow B\) and \(B \Rightarrow A\), whose the truth value is false when the truth values of the antecedent and the consequent are respectively true and false.
  • It is sometimes necessary to click twice on Prove button.

    Enjoy !

A - Prolog Code:

D - Examples of Queries:

  1. Excluded Middle: a | ~ a
  2. Dilemma : ((~ a => b) & (a => b)) => b
  3. Double Negation: ~(~a) <=> a
  4. Peirce’s Law: ((a => b) => a) => a
  5. Dummett Formula : (a => b)| (b => a)
  6. Classical equivalence for negation : (~a => a) <=> a
  7. Classical De Morgan's Law : ~((a & b)) => (~ a | ~b)
  8. Pelletier Problem 17 : ( ( ( p & ( q => r ) ) => s ) <=> ( ( ~ p | q | s ) & ( ~ p | ~ r | s ) ) )
  9. a
  10. a => b
  11. (a | b) => (a & b)
  12. a & b | a & ~b | ~a & b | ~a & ~c

2. Source Code

  • The file of this Prolog prover is here.
  • The html code of this web page has been produced with org-mode. Its .org file source is here and contains the Tau-Prolog script to get sequent proofs that we can see on web pages thanks to MathJax.

3. Efficiency

The code of this prover is SWI Prolog’s. Pelletier Problem 71 that is formula on file SYN007+1.014.p of ILTP Problems Library can be solved by this prover with the following statistics: 54,890,489 inferences, 4.558 CPU in 4.561 seconds (100% CPU, 12042963 Lips). In comparison, for the same formula, Vampire needs only 0.073 seconds to conclude that this formula is a theorem. But the fact that this Prolog prover succeeds in proving this formula shows that it is nevertheless rather efficient.

4. TODO

  • This prover online for First-Order Logic.
  • A SWI-Prolog LaTeX printer for bussproofs.

5. References

[1]
David, R. et al.: Introduction à la logique: théorie de la démonstration. Paris: Dunod, 2004.
[2]
Wang, H.: Toward mechanical mathematics. Ibm j. res. dev., 4 (1), 1960, p. 2–22.
[3]
 

Made with Emacs 29.0.50 (Org mode 9.5) and with org-export-head, a blog exporter.

The css file of this blog is mainly the result of Zhitao Gong's work.

orgmode emacs isso debian mxlinux