Skip to Main content Skip to Navigation
Journal articles

Formalizing Bachmair and Ganzinger’s Ordered Resolution Prover

Abstract : 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.
Document type :
Journal articles
Complete list of metadata
Contributor : Stephan Merz Connect in order to contact the contributor
Submitted on : Wednesday, February 17, 2021 - 4:12:20 PM
Last modification on : Wednesday, November 3, 2021 - 7:09:22 AM
Long-term archiving on: : Tuesday, May 18, 2021 - 7:37:20 PM


Files produced by the author(s)




Anders Schlichtkrull, Jasmin Blanchette, Dmitriy Traytel, Uwe Waldmann. Formalizing Bachmair and Ganzinger’s Ordered Resolution Prover. Journal of Automated Reasoning, Springer Verlag, 2020, 64 (7), pp.1169-1195. ⟨10.1007/s10817-020-09561-0⟩. ⟨hal-03144467⟩



Les métriques sont temporairement indisponibles