Journal article
Formalization of the Resolution Calculus for First-Order Logic
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.
Language: | English |
---|---|
Publisher: | Springer Netherlands |
Year: | 2018 |
Pages: | 455-484 |
ISSN: | 15730670 and 01687433 |
Types: | Journal article |
DOI: | 10.1007/s10817-017-9447-z |
ORCIDs: | Schlichtkrull, Anders |