|
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 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.
|
|