Formalizing Bachmair and Ganzinger’s Ordered Resolution Prover

Anders Schlichtkrull*, Jasmin Blanchette, Dmitriy Traytel, Uwe Waldmann

*Corresponding author for this work

Research output: Contribution to JournalArticleAcademicpeer-review

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.

Original languageEnglish
Pages (from-to)1169-1195
Number of pages27
JournalJournal of Automated Reasoning
Volume64
Issue number7
Early online date17 Jun 2020
DOIs
Publication statusPublished - Oct 2020

Keywords

  • Automatic theorem provers
  • Proof assistants
  • Resolution calculus

Fingerprint Dive into the research topics of 'Formalizing Bachmair and Ganzinger’s Ordered Resolution Prover'. Together they form a unique fingerprint.

  • Cite this