Download PDFOpen PDF in browser

Formalizing Bachmair and Ganzinger's Ordered Resolution Prover

EasyChair Preprint no. 396

16 pagesDate: August 3, 2018


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.

Keyphrases: completeness, first-order logic, Isabelle/HOL, proof assistant, prover, resolution

BibTeX entry
BibTeX does not have the right entry for preprints. This is a hack for producing the correct reference:
  author = {Anders Schlichtkrull and Jasmin Christian Blanchette and Dmitriy Traytel and Uwe Waldmann},
  title = {Formalizing Bachmair and Ganzinger's Ordered Resolution Prover},
  howpublished = {EasyChair Preprint no. 396},
  doi = {10.29007/pn71},
  year = {EasyChair, 2018}}
Download PDFOpen PDF in browser