A Verified Functional Implementation of Bachmair and Ganzinger’s Ordered Resolution Prover

Anders Schlichtkrull; Jasmin Christian Blanchette; Dmitriy Traytel

A Verified Functional Implementation of Bachmair and Ganzinger’s Ordered Resolution Prover

Anders Schlichtkrull
, Jasmin Christian Blanchette
, Dmitriy Traytel

Department of Applied Mathematics and Computer Science

Vrije Universiteit Amsterdam
Swiss Federal Institute of Technology Zurich

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

140 Downloads (Orbit)

Abstract

This Isabelle/HOL formalization refines the abstract ordered resolution prover presented in Section 4.3 of Bachmair and Ganzinger’s “Resolution Theorem Proving” chapter in the Handbook of Automated Reasoning. The result is a functional implementation of a first-order prover.

Original language	English
Book series	Archive of Formal Proofs
Pages (from-to)	1-60
ISSN	2150-914X
Publication status	Published - 2018

Access to Document

Document 4 Final published version, 510 KB

OpenUrl availability

Check availability in DTU Findit

Cite this

@article{38b9d188c4b149438ccb78640783e8ba,

title = "A Verified Functional Implementation of Bachmair and Ganzinger{\textquoteright}s Ordered Resolution Prover",

abstract = "This Isabelle/HOL formalization refines the abstract ordered resolution prover presented in Section 4.3 of Bachmair and Ganzinger{\textquoteright}s “Resolution Theorem Proving” chapter in the Handbook of Automated Reasoning. The result is a functional implementation of a first-order prover.",

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

year = "2018",

language = "English",

pages = "1--60",

journal = "Archive of Formal Proofs",

issn = "2150-914X",

publisher = "SourceForge",

}

TY - JOUR

T1 - A Verified Functional Implementation of Bachmair and Ganzinger’s Ordered Resolution Prover

AU - Schlichtkrull, Anders

AU - Blanchette, Jasmin Christian

AU - Traytel, Dmitriy

PY - 2018

Y1 - 2018

N2 - This Isabelle/HOL formalization refines the abstract ordered resolution prover presented in Section 4.3 of Bachmair and Ganzinger’s “Resolution Theorem Proving” chapter in the Handbook of Automated Reasoning. The result is a functional implementation of a first-order prover.

AB - This Isabelle/HOL formalization refines the abstract ordered resolution prover presented in Section 4.3 of Bachmair and Ganzinger’s “Resolution Theorem Proving” chapter in the Handbook of Automated Reasoning. The result is a functional implementation of a first-order prover.

M3 - Journal article

SN - 2150-914X

SP - 1

EP - 60

JO - Archive of Formal Proofs

JF - Archive of Formal Proofs

ER -

A Verified Functional Implementation of Bachmair and Ganzinger’s Ordered Resolution Prover

Abstract

Access to Document

OpenUrl availability

Fingerprint

Cite this