Formalization of the Resolution Calculus for First-Order Logic

Research output: Research - peer-reviewJournal article – Annual report year: 2018

View graph of relations

I present a formalization in Isabelle/HOL of the resolution calculus for first-order logic with formal soundness and completeness proofs. To prove the calculus sound, I use the substitution lemma, and to prove it complete, I use Herbrand interpretations and semantic trees. The correspondence between unsatisfiable sets of clauses and finite semantic trees is formalized in Herbrand’s theorem. I discuss the difficulties that I had formalizing proofs of the lifting lemma found in the literature, and I formalize a correct proof. The completeness proof is by induction on the size of a finite semantic tree. Throughout the paper I emphasize details that are often glossed over in paper proofs. I give a thorough overview of formalizations of first-order logic found in the literature. The formalization of resolution is part of the IsaFoL project, which is an effort to formalize logics in Isabelle/HOL.

Original languageEnglish
JournalJournal of Automated Reasoning
Volume61
Issue number1–4
Pages (from-to)455–484
ISSN0168-7433
DOIs
StatePublished - 20 Jan 2018
CitationsWeb of Science® Times Cited: 0

    Research areas

  • Completeness, First-order logic, Herbrand’s theorem, Isabelle/HOL, Resolution, Semantic trees, Soundness
Download as:
Download as PDF
Select render style:
APAAuthorCBE/CSEHarvardMLAStandardVancouverShortLong
PDF
Download as HTML
Select render style:
APAAuthorCBE/CSEHarvardMLAStandardVancouverShortLong
HTML
Download as Word
Select render style:
APAAuthorCBE/CSEHarvardMLAStandardVancouverShortLong
Word

ID: 143091546