Abstract
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.
Cite
CITATION STYLE
Schlichtkrull, A., Blanchette, J. C., Traytel, D., & Waldmann, U. (2018). Formalizing Bachmair and Ganzinger’s Ordered Resolution Prover. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 10900 LNAI, pp. 89–107). Springer Verlag. https://doi.org/10.1007/978-3-319-94205-6_7
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
