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 in the Journal of Automated Reasoning [Sch18] which extends a paper presented at the International Conference on Interactive Theorem Proving [Sch16]. An earlier version was presented in an MSc thesis [Sch15]. The formalization mostly follows textbooks by Ben-Ari [BA12], Chang and Lee [CL73], and Leitsch [Lei97]. The theory is part of the IsaFoL project [IsaFoL]. [Sch18] Anders Schlichtkrull. "Formalization of the Resolution Calculus for First-Order Logic". Journal of Automated Reasoning, 2018. [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. [IsaFoL] IsaFoL authors. IsaFoL: Isabelle Formalization of Logic. https://bitbucket.org/jasmin_blanchette/isafol.
Change history:	[2018-01-24]: added several new versions of the soundness and completeness theorems as described in the paper [Sch18]. [2018-03-20]: added a concrete instance of the unification and completeness theorems using the First-Order Terms AFP-entry from IsaFoR as described in the papers [Sch16] and [Sch18].
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.html}, Formal proof development}, ISSN = {2150-914x}, }
License:	BSD License
Depends on:	First_Order_Terms
Status: [ok]	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