Abstract
A formalization in Isabelle/HOL of the resolution calculus for first-order logic is presented. Its soundness and completeness are formally proven using the substitution lemma, semantic trees, Herbrand’s theorem, and the lifting lemma. In contrast to previous formalizations of resolution, it considers first-order logic with full first-order terms, instead of the propositional case.
| Original language | English |
|---|---|
| Title of host publication | Proceedings of the 7th International Conference on Interactive Theorem Proving (ITP 2016) |
| Editors | Jasmin Christian Blanchette, Stephan Merz |
| Publisher | Springer |
| Publication date | 2016 |
| Pages | 341-357 |
| ISBN (Print) | 978-3-319-43143-7 |
| ISBN (Electronic) | 978-3-319-43144-4 |
| DOIs | |
| Publication status | Published - 2016 |
| Event | 7th International Conference on Interactive Theorem Proving (ITP 2016) - Nancy, France Duration: 22 Aug 2016 → 25 Aug 2016 Conference number: 7 https://itp2016.inria.fr/ |
Conference
| Conference | 7th International Conference on Interactive Theorem Proving (ITP 2016) |
|---|---|
| Number | 7 |
| Country/Territory | France |
| City | Nancy |
| Period | 22/08/2016 → 25/08/2016 |
| Internet address |
| Series | Lecture Notes in Computer Science |
|---|---|
| Volume | 9807 |
| ISSN | 0302-9743 |
Keywords
- First-order logic
- Resolution
- Isabelle/HOL
- Herbrand’s theorem
- Soundness
- Completeness