Conference paper · Book chapter
Formalizing Bachmair and Ganzinger’s Ordered Resolution Prover
Department of Applied Mathematics and Computer Science, Technical University of Denmark1
Algorithms and Logic, Department of Applied Mathematics and Computer Science, Technical University of Denmark2
Vrije Universiteit Amsterdam3
Swiss Federal Institute of Technology Zurich4
Saarland University5
We present a formalization of the first half of Bachmair and Ganzinger’s chapter on resolution theorem proving in Isabelle/HOL, culminating with a refutationally complete first-order prover based on ordered resolution with literal selection. We develop general infrastructure and methodology that can form the basis of completeness proofs for related calculi, including superposition.
Our work clarifies several of the fine points in the chapter’s text, emphasizing the value of formal proofs in the field of automated reasoning.
| Language: | English |
|---|---|
| Publisher: | Springer |
| Year: | 2018 |
| Pages: | 89-107 |
| Proceedings: | 9<sup>th</sup> International Joint Conference on Automated Reasoning |
| Series: | Lecture Notes in Computer Science |
| Journal subtitle: | 9th International Joint Conference, Ijcar 2018, Held As Part of the Federated Logic Conference, Floc 2018, Oxford, Uk, July 14-17, 2018, Proceedings |
| ISBN: | 3319942042 , 3319942050 , 9783319942049 and 9783319942056 |
| ISSN: | 03029743 and 16113349 |
| Types: | Conference paper and Book chapter |
| DOI: | 10.1007/978-3-319-94205-6_7 |
| ORCIDs: | Schlichtkrull, Anders |
