Email Gateway (Aug 22 2022 at 13:30): Email Gateway (Aug 22 2022 at 13:30):From: Tobias Nipkow <nipkow@in.tum.de>
The Resolution Calculus for First-Order Logic
Anders Schlichtkrull
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 at the International Conference on Interactive Theorem
Proving [Sch16] and an earlier version in an MSc thesis [Sch15]. It mostly
follows textbooks by Ben-Ari [BA12], Chang and Lee [CL73], and Leitsch [Lei97].
The theory is part of the IsaFoL project [Bla+].
https://www.isa-afp.org/entries/Resolution_FOL.shtml
Enjoy!
smime.p7s
Last updated: Apr 24 2024 at 16:18 UTC