
The
Resolution
Calculus
for
FirstOrder
Logic
Title: 
The Resolution Calculus for FirstOrder Logic 
Author:

Anders Schlichtkrull

Submission date: 
20160630 
Abstract: 
This theory is a formalization of the resolution calculus for
firstorder 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 firstorder 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 BenAri [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
FirstOrder 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 BenAri. Mathematical Logic for
Computer Science. 3rd. Springer, 2012. [CL73] ChinLiang Chang and Richard CharTung 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_FOLAFP,
author = {Anders Schlichtkrull},
title = {The Resolution Calculus for FirstOrder Logic},
journal = {Archive of Formal Proofs},
month = jun,
year = 2016,
note = {\url{http://isaafp.org/entries/Resolution_FOL.shtml},
Formal proof development},
ISSN = {2150914x},
}

License: 
BSD License 
