The Resolution Calculus for First-Order Logic

Research output: Contribution to journalJournal articleResearchpeer-review

201 Downloads (Pure)

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 unsatis able set of clauses has a nite 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 [7] and an earlier version in an MSc thesis [6]. It mostly follows textbooks by Ben-Ari [1], Chang and Lee [3], and Leitsch [4]. The theory is part of the IsaFoL project [2].
Original languageEnglish
Book seriesArchive of Formal Proofs
Pages (from-to)1-69
ISSN2150-914X
Publication statusPublished - 2016

Fingerprint Dive into the research topics of 'The Resolution Calculus for First-Order Logic'. Together they form a unique fingerprint.

Cite this