| ||||
| ||||
![]() Title:Formalizing Bachmair and Ganzinger's Ordered Resolution Prover Conference:IJCAR-2018 Tags:completeness, first-order logic, Isabelle/HOL, proof assistant, prover and resolution 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. 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. Formalizing Bachmair and Ganzinger's Ordered Resolution Prover ![]() Formalizing Bachmair and Ganzinger's Ordered Resolution Prover | ||||
Copyright © 2002 – 2025 EasyChair |