Formalizing Bachmair and Ganzinger's Ordered Resolution Prover
Research output: Contribution to journal › Journal article › Research › peer-review
Standard
Formalizing Bachmair and Ganzinger's Ordered Resolution Prover. / Schlichtkrull, Anders; Blanchette, Jasmin Christian; Traytel, Dmitriy; Waldmann, Uwe.
In: Journal of Automated Reasoning, Vol. 64, 2020, p. 1169–1195.Research output: Contribution to journal › Journal article › Research › peer-review
Harvard
APA
Vancouver
Author
Bibtex
}
RIS
TY - JOUR
T1 - Formalizing Bachmair and Ganzinger's Ordered Resolution Prover
AU - Schlichtkrull, Anders
AU - Blanchette, Jasmin Christian
AU - Traytel, Dmitriy
AU - Waldmann, Uwe
PY - 2020
Y1 - 2020
N2 - We present an Isabelle/HOL formalization of the first half of Bachmair and Ganzinger’s chapter on resolution theorem proving, culminating with a refutationally complete first-order prover based on ordered resolution with literal selection. We developed general infrastructure and methodology that can form the basis of completeness proofs for related calculi, including superposition. Our work clarifies fine points in the chapter, emphasizing the value of formal proofs in the field of automated reasoning.
AB - We present an Isabelle/HOL formalization of the first half of Bachmair and Ganzinger’s chapter on resolution theorem proving, culminating with a refutationally complete first-order prover based on ordered resolution with literal selection. We developed general infrastructure and methodology that can form the basis of completeness proofs for related calculi, including superposition. Our work clarifies fine points in the chapter, emphasizing the value of formal proofs in the field of automated reasoning.
U2 - 10.1007/s10817-020-09561-0
DO - 10.1007/s10817-020-09561-0
M3 - Journal article
VL - 64
SP - 1169
EP - 1195
JO - Journal of Automated Reasoning
JF - Journal of Automated Reasoning
SN - 0168-7433
ER -
ID: 245667075