Formalization of Bachmair and Ganzinger's Ordered Resolution Prover

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

Research output: Contribution to journalJournal articleResearchpeer-review

240 Downloads (Pure)

Abstract

This Isabelle/HOL formalization covers Sections 2 to 4 of Bachmair and Ganzinger’s “Resolution Theorem Proving” chapter in the Handbook of Automated Reasoning. This includes soundness and completeness of unordered and ordered variants of ground resolution with and without literal selection, the standard redundancy criterion, a general framework for refutational theorem proving, and soundness and completeness of an abstract first-order prover.
Original languageEnglish
Book seriesArchive of Formal Proofs
Pages (from-to)1-117
ISSN2150-914X
Publication statusPublished - 2018

Bibliographical note

https://www.isa-afp.org/entries/Ordered_Resolution_Prover.html

Fingerprint

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

Cite this