The Resolution Calculus for First-Order Logic


Title: The Resolution Calculus for First-Order Logic
Author: Anders Schlichtkrull (andschl /at/ dtu /dot/ dk)
Submission date: 2016-06-30
Abstract: This theory is a formalization of the resolution calculus for first-order logic. It is proven sound and complete. The soundness proof uses the substitution lemma, which shows a correspondence between substitutions and updates to an environment. The completeness proof uses semantic trees, i.e. trees whose paths are partial Herbrand interpretations. It employs Herbrand's theorem in a formulation which states that an unsatisfiable set of clauses has a finite closed semantic tree. It also uses the lifting lemma which lifts resolution derivation steps from the ground world up to the first-order world. The theory is presented in a paper at the International Conference on Interactive Theorem Proving [Sch16] and an earlier version in an MSc thesis [Sch15]. It mostly follows textbooks by Ben-Ari [BA12], Chang and Lee [CL73], and Leitsch [Lei97]. The theory is part of the IsaFoL project [Bla+].

[Sch16] Anders Schlichtkrull. "Formalization of the Resolution Calculus for First-Order Logic". In: ITP 2016. Vol. 9807. LNCS. Springer, 2016.
[Sch15] Anders Schlichtkrull. "Formalization of Resolution Calculus in Isabelle". MSc thesis. Technical University of Denmark, 2015.
[BA12] Mordechai Ben-Ari. Mathematical Logic for Computer Science. 3rd. Springer, 2012.
[CL73] Chin-Liang Chang and Richard Char-Tung Lee. Symbolic Logic and Mechanical Theorem Proving. 1st. Academic Press, Inc., 1973.
[Lei97] Alexander Leitsch. The Resolution Calculus. Texts in theoretical computer science. Springer, 1997.
[Bla+] J. C. Blanchette, M. Fleury, A. Schlichtkrull, and D. Traytel. IsaFoL: Isabelle Formalization of Logic.

  author  = {Anders Schlichtkrull},
  title   = {The Resolution Calculus for First-Order Logic},
  journal = {Archive of Formal Proofs},
  month   = jun,
  year    = 2016,
  note    = {\url{},
            Formal proof development},
  ISSN    = {2150-914x},
License: BSD License