## Abstract

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 language | English |
---|---|

Journal | Journal of Automated Reasoning |

Volume | 61 |

Issue number | 1–4 |

Pages (from-to) | 455–484 |

ISSN | 0168-7433 |

DOIs | |

Publication status | Published - 20 Jan 2018 |

## Keywords

- Completeness
- First-order logic
- Herbrand’s theorem
- Isabelle/HOL
- Resolution
- Semantic trees
- Soundness