TY - GEN
T1 - Formalizing Bachmair and Ganzinger’s Ordered Resolution Prover
AU - Schlichtkrull, Anders
AU - Blanchette, Jasmin Christian
AU - Traytel, Dmitriy
AU - Waldmann, Uwe
PY - 2018
Y1 - 2018
N2 - 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.
AB - 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.
UR - http://www.scopus.com/inward/record.url?scp=85049975238&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=85049975238&partnerID=8YFLogxK
U2 - 10.1007/978-3-319-94205-6_7
DO - 10.1007/978-3-319-94205-6_7
M3 - Conference contribution
AN - SCOPUS:85049975238
SN - 9783319942049
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 89
EP - 107
BT - Automated Reasoning
PB - Springer/Verlag
T2 - 9th International Joint Conference on Automated Reasoning, IJCAR 2018 Held as Part of the Federated Logic Conference, FloC 2018
Y2 - 14 July 2018 through 17 July 2018
ER -