Home
About
Submission
Updating Entries
Using Entries
Search
Statistics
Index
Download

 

 

 

The Resolution Calculus for First-Order Logic

 

Title: The Resolution Calculus for First-Order Logic
Author: Anders Schlichtkrull
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". https://people.compute.dtu.dk/andschl/Thesis.pdf. 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. https://bitbucket.org/jasmin_blanchette/isafol.
BibTeX: 
@article{Resolution_FOL-AFP,
  author  = {Anders Schlichtkrull},
  title   = {The Resolution Calculus for First-Order Logic},
  journal = {Archive of Formal Proofs},
  month   = jun,
  year    = 2016,
  note    = {\url{http://isa-afp.org/entries/Resolution_FOL.shtml},
            Formal proof development},
  ISSN    = {2150-914x},
}
License: BSD License
Status: [skipped] This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.

Proof outline
Proof document
Browse theories
Download this entry
Older releases: