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

https://hal.inria.fr/hal-03144467
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

File

paper.pdf
Files produced by the author(s)

Identifiers

Collections

Citation

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⟩

Share

Metrics

Les métriques sont temporairement indisponibles