Formalizing Bachmair and Ganzinger’s Ordered Resolution Prover

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

Research output: Chapter in Book / Report / Conference proceedingConference contributionAcademicpeer-review

Abstract

We present a formalization of the first half of Bachmair and Ganzinger’s chapter on resolution theorem proving in Isabelle/HOL, culminating with a refutationally complete first-order prover based on ordered resolution with literal selection. We develop general infrastructure and methodology that can form the basis of completeness proofs for related calculi, including superposition. Our work clarifies several of the fine points in the chapter’s text, emphasizing the value of formal proofs in the field of automated reasoning.

Original languageEnglish
Title of host publicationAutomated Reasoning - 9th International Joint Conference, IJCAR 2018, Held as Part of the Federated Logic Conference, FloC 2018, Proceedings
PublisherSpringer/Verlag
Pages89-107
Number of pages19
ISBN (Electronic)9783319942056
ISBN (Print)9783319942049
DOIs
Publication statusPublished - 2018
Event9th International Joint Conference on Automated Reasoning, IJCAR 2018 Held as Part of the Federated Logic Conference, FloC 2018 - Oxford, United Kingdom
Duration: 14 Jul 201817 Jul 2018

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume10900 LNAI
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Conference

Conference9th International Joint Conference on Automated Reasoning, IJCAR 2018 Held as Part of the Federated Logic Conference, FloC 2018
CountryUnited Kingdom
CityOxford
Period14/07/1817/07/18

Fingerprint

Theorem proving
Automated Reasoning
Formal Proof
Theorem Proving
Formalization
Superposition
Completeness
Calculus
Infrastructure
First-order
Methodology
Text

Cite this

Schlichtkrull, A., Blanchette, J. C., Traytel, D., & Waldmann, U. (2018). Formalizing Bachmair and Ganzinger’s Ordered Resolution Prover. In Automated Reasoning - 9th International Joint Conference, IJCAR 2018, Held as Part of the Federated Logic Conference, FloC 2018, Proceedings (pp. 89-107). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 10900 LNAI). Springer/Verlag. https://doi.org/10.1007/978-3-319-94205-6_7
Schlichtkrull, Anders ; Blanchette, Jasmin Christian ; Traytel, Dmitriy ; Waldmann, Uwe. / Formalizing Bachmair and Ganzinger’s Ordered Resolution Prover. Automated Reasoning - 9th International Joint Conference, IJCAR 2018, Held as Part of the Federated Logic Conference, FloC 2018, Proceedings. Springer/Verlag, 2018. pp. 89-107 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).
@inproceedings{3cdb8c944aee4997a5342f50fb245a16,
title = "Formalizing Bachmair and Ganzinger’s Ordered Resolution Prover",
abstract = "We present a formalization of the first half of Bachmair and Ganzinger’s chapter on resolution theorem proving in Isabelle/HOL, culminating with a refutationally complete first-order prover based on ordered resolution with literal selection. We develop general infrastructure and methodology that can form the basis of completeness proofs for related calculi, including superposition. Our work clarifies several of the fine points in the chapter’s text, emphasizing the value of formal proofs in the field of automated reasoning.",
author = "Anders Schlichtkrull and Blanchette, {Jasmin Christian} and Dmitriy Traytel and Uwe Waldmann",
year = "2018",
doi = "10.1007/978-3-319-94205-6_7",
language = "English",
isbn = "9783319942049",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
publisher = "Springer/Verlag",
pages = "89--107",
booktitle = "Automated Reasoning - 9th International Joint Conference, IJCAR 2018, Held as Part of the Federated Logic Conference, FloC 2018, Proceedings",

}

Schlichtkrull, A, Blanchette, JC, Traytel, D & Waldmann, U 2018, Formalizing Bachmair and Ganzinger’s Ordered Resolution Prover. in Automated Reasoning - 9th International Joint Conference, IJCAR 2018, Held as Part of the Federated Logic Conference, FloC 2018, Proceedings. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 10900 LNAI, Springer/Verlag, pp. 89-107, 9th International Joint Conference on Automated Reasoning, IJCAR 2018 Held as Part of the Federated Logic Conference, FloC 2018, Oxford, United Kingdom, 14/07/18. https://doi.org/10.1007/978-3-319-94205-6_7

Formalizing Bachmair and Ganzinger’s Ordered Resolution Prover. / Schlichtkrull, Anders; Blanchette, Jasmin Christian; Traytel, Dmitriy; Waldmann, Uwe.

Automated Reasoning - 9th International Joint Conference, IJCAR 2018, Held as Part of the Federated Logic Conference, FloC 2018, Proceedings. Springer/Verlag, 2018. p. 89-107 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 10900 LNAI).

Research output: Chapter in Book / Report / Conference proceedingConference contributionAcademicpeer-review

TY - GEN

T1 - Formalizing Bachmair and Ganzinger’s Ordered Resolution Prover

AU - Schlichtkrull, Anders

AU - Blanchette, Jasmin Christian

AU - Traytel, Dmitriy

AU - Waldmann, Uwe

PY - 2018

Y1 - 2018

N2 - We present a formalization of the first half of Bachmair and Ganzinger’s chapter on resolution theorem proving in Isabelle/HOL, culminating with a refutationally complete first-order prover based on ordered resolution with literal selection. We develop general infrastructure and methodology that can form the basis of completeness proofs for related calculi, including superposition. Our work clarifies several of the fine points in the chapter’s text, emphasizing the value of formal proofs in the field of automated reasoning.

AB - We present a formalization of the first half of Bachmair and Ganzinger’s chapter on resolution theorem proving in Isabelle/HOL, culminating with a refutationally complete first-order prover based on ordered resolution with literal selection. We develop general infrastructure and methodology that can form the basis of completeness proofs for related calculi, including superposition. Our work clarifies several of the fine points in the chapter’s text, emphasizing the value of formal proofs in the field of automated reasoning.

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

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

U2 - 10.1007/978-3-319-94205-6_7

DO - 10.1007/978-3-319-94205-6_7

M3 - Conference contribution

SN - 9783319942049

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 89

EP - 107

BT - Automated Reasoning - 9th International Joint Conference, IJCAR 2018, Held as Part of the Federated Logic Conference, FloC 2018, Proceedings

PB - Springer/Verlag

ER -

Schlichtkrull A, Blanchette JC, Traytel D, Waldmann U. Formalizing Bachmair and Ganzinger’s Ordered Resolution Prover. In Automated Reasoning - 9th International Joint Conference, IJCAR 2018, Held as Part of the Federated Logic Conference, FloC 2018, Proceedings. Springer/Verlag. 2018. p. 89-107. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). https://doi.org/10.1007/978-3-319-94205-6_7