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

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

269 Downloads (Orbit)

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
Journal	Journal of Automated Reasoning
Issue number	Special Issue: Selected Extended Papers from IJCAR 2018
Pages (from-to)	1-27
ISSN	0168-7433
DOIs	https://doi.org/10.1007/s10817-020-09561-0
Publication status	Published - 2020

Keywords

Resolution calculus
Automatic theorem provers
Proof assistants

Access to Document

10.1007/s10817-020-09561-0

FulltextAccepted author manuscript, 267 KB

https://rdcu.be/b5Jmo

OpenUrl availability

Check availability in DTU Findit

Cite this

@article{8a4059cd97fd484eb7aab79ea0609b71,

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 = "Resolution calculus, Automatic theorem provers, Proof assistants",

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

year = "2020",

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

language = "English",

pages = "1--27",

journal = "Journal of Automated Reasoning",

issn = "0168-7433",

publisher = "Springer Netherlands",

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

}

TY - JOUR

T1 - Formalizing Bachmair and Ganzinger’s Ordered Resolution Prover

AU - Schlichtkrull, Anders

AU - Blanchette, Jasmin

AU - Traytel, Dmitriy

AU - Waldmann, Uwe

PY - 2020

Y1 - 2020

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 - Resolution calculus

KW - Automatic theorem provers

KW - Proof assistants

U2 - 10.1007/s10817-020-09561-0

DO - 10.1007/s10817-020-09561-0

M3 - Journal article

SN - 0168-7433

SP - 1

EP - 27

JO - Journal of Automated Reasoning

JF - Journal of Automated Reasoning

IS - Special Issue: Selected Extended Papers from IJCAR 2018

ER -

Formalizing Bachmair and Ganzinger’s Ordered Resolution Prover

Abstract

Keywords

Access to Document

OpenUrl availability

Fingerprint

Cite this