Formalization of Bachmair and Ganzinger's Ordered Resolution Prover

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

Formalization of Bachmair and Ganzinger's Ordered Resolution Prover

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

Department of Applied Mathematics and Computer Science

Vrije Universiteit Amsterdam
Swiss Federal Institute of Technology Zurich
Max Planck Institute for Informatics

Research output: Contribution to journal › Journal article › Research › peer-review

315 Downloads (Orbit)

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 language	English
Book series	Archive of Formal Proofs
Pages (from-to)	1-117
ISSN	2150-914X
Publication status	Published - 2018

Bibliographical note

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

Access to Document

Document 2 Final published version, 745 KB

OpenUrl availability

Check availability in DTU Findit

Cite this

@article{1d1de0bce3074006b6a93a355889ef21,

title = "Formalization of Bachmair and Ganzinger's Ordered Resolution Prover",

abstract = "This Isabelle/HOL formalization covers Sections 2 to 4 of Bachmair and Ganzinger{\textquoteright}s {\textquotedblleft}Resolution Theorem Proving{\textquotedblright} 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. ",

author = "Anders Schlichtkrull and Blanchette, \{Jasmin Christian\} and Dmitriy Traytel and Uwe Waldmann",

note = "https://www.isa-afp.org/entries/Ordered\_Resolution\_Prover.html",

year = "2018",

language = "English",

pages = "1--117",

journal = "Archive of Formal Proofs",

issn = "2150-914X",

publisher = "SourceForge",

}

TY - JOUR

T1 - Formalization of Bachmair and Ganzinger's Ordered Resolution Prover

AU - Schlichtkrull, Anders

AU - Blanchette, Jasmin Christian

AU - Traytel, Dmitriy

AU - Waldmann, Uwe

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

PY - 2018

Y1 - 2018

N2 - 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.

AB - 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.

M3 - Journal article

SN - 2150-914X

SP - 1

EP - 117

JO - Archive of Formal Proofs

JF - Archive of Formal Proofs

ER -

Formalization of Bachmair and Ganzinger's Ordered Resolution Prover

Abstract

Bibliographical note

Access to Document

OpenUrl availability

Fingerprint

Cite this