Formalizing Bachmair and Ganzinger’s Ordered Resolution Prover

Anders Schlichtkrull; Jasmin Blanchette; Dmitriy Traytel; Uwe Waldmann

doi:10.1007/s10817-020-09561-0

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 Journal › Article › Academic › peer-review

167 Downloads (Pure)

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 language	English
Pages (from-to)	1169-1195
Number of pages	27
Journal	Journal of Automated Reasoning
Volume	64
Issue number	7
Early online date	17 Jun 2020
DOIs	https://doi.org/10.1007/s10817-020-09561-0
Publication status	Published - Oct 2020

Bibliographical note

Special Issue: Selected Extended Papers from IJCAR 2018.

Keywords

Automatic theorem provers
Proof assistants
Resolution calculus

Access to Document

10.1007/s10817-020-09561-0

Schlichtkrull2020_Formalizing Bachmair and Ganzingers Ordered Resolution ProverFinal published version, 362 KBLicence: Article 25fa Dutch Copyright Act

Handle.net

Persistent link

Cite this

@article{09bae484e3f34ea4a2a677e59679a235,

title = "Formalizing Bachmair and Ganzinger{\textquoteright}s Ordered Resolution Prover",

abstract = "We present an Isabelle/HOL formalization of the first half of Bachmair and Ganzinger{\textquoteright}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.",

keywords = "Automatic theorem provers, Proof assistants, Resolution calculus",

author = "Anders Schlichtkrull and Jasmin Blanchette and Dmitriy Traytel and Uwe Waldmann",

note = "Special Issue: Selected Extended Papers from IJCAR 2018.",

year = "2020",

month = oct,

doi = "10.1007/s10817-020-09561-0",

language = "English",

volume = "64",

pages = "1169--1195",

journal = "Journal of Automated Reasoning",

issn = "0168-7433",

publisher = "Springer Netherlands",

number = "7",

}

TY - JOUR

T1 - Formalizing Bachmair and Ganzinger’s Ordered Resolution Prover

AU - Schlichtkrull, Anders

AU - Blanchette, Jasmin

AU - Traytel, Dmitriy

AU - Waldmann, Uwe

N1 - Special Issue: Selected Extended Papers from IJCAR 2018.

PY - 2020/10

Y1 - 2020/10

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

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

KW - Automatic theorem provers

KW - Proof assistants

KW - Resolution calculus

UR - http://www.scopus.com/inward/record.url?scp=85086643610&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=85086643610&partnerID=8YFLogxK

U2 - 10.1007/s10817-020-09561-0

DO - 10.1007/s10817-020-09561-0

M3 - Article

AN - SCOPUS:85086643610

VL - 64

SP - 1169

EP - 1195

JO - Journal of Automated Reasoning

JF - Journal of Automated Reasoning

SN - 0168-7433

IS - 7

ER -

Formalizing Bachmair and Ganzinger’s Ordered Resolution Prover

Abstract

Bibliographical note

Keywords

Access to Document

Handle.net

Other files and links

Fingerprint

Cite this