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  and an earlier version in an MSc thesis . It mostly follows textbooks by Ben-Ari , Chang and Lee , and Leitsch . The theory is part of the IsaFoL project .
|Archive of Formal Proofs
|Published - 2016