Formalizing Bachmair and Ganzinger's Ordered Resolution Prover

Publikation: Bidrag til tidsskrift › Tidsskriftartikel › Forskning › fagfællebedømt

Standard

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

I: Journal of Automated Reasoning, Bind 64, 2020, s. 1169–1195.

Publikation: Bidrag til tidsskrift › Tidsskriftartikel › Forskning › fagfællebedømt

Harvard

Schlichtkrull, A, Blanchette, JC, Traytel, D & Waldmann, U 2020, 'Formalizing Bachmair and Ganzinger's Ordered Resolution Prover', Journal of Automated Reasoning, bind 64, s. 1169–1195. https://doi.org/10.1007/s10817-020-09561-0

APA

Schlichtkrull, A., Blanchette, J. C., Traytel, D., & Waldmann, U. (2020). Formalizing Bachmair and Ganzinger's Ordered Resolution Prover. Journal of Automated Reasoning, 64, 1169–1195. https://doi.org/10.1007/s10817-020-09561-0

Vancouver

Schlichtkrull A, Blanchette JC, Traytel D, Waldmann U. Formalizing Bachmair and Ganzinger's Ordered Resolution Prover. Journal of Automated Reasoning. 2020;64:1169–1195. https://doi.org/10.1007/s10817-020-09561-0

Author

Schlichtkrull, Anders ; Blanchette, Jasmin Christian ; Traytel, Dmitriy ; Waldmann, Uwe. / Formalizing Bachmair and Ganzinger's Ordered Resolution Prover. I: Journal of Automated Reasoning. 2020 ; Bind 64. s. 1169–1195.

Bibtex

@article{46aaa51b94e648e0a579fcae82456a45,
title = "Formalizing Bachmair and Ganzinger'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.",
author = "Anders Schlichtkrull and Blanchette, {Jasmin Christian} and Dmitriy Traytel and Uwe Waldmann",
year = "2020",
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",

}

RIS

TY - JOUR

T1 - Formalizing Bachmair and Ganzinger's Ordered Resolution Prover

AU - Schlichtkrull, Anders

AU - Blanchette, Jasmin Christian

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.

U2 - 10.1007/s10817-020-09561-0

DO - 10.1007/s10817-020-09561-0

M3 - Journal article

VL - 64

SP - 1169

EP - 1195

JO - Journal of Automated Reasoning

JF - Journal of Automated Reasoning

SN - 0168-7433

ER -

ID: 245667075