Formalizing Bachmair and Ganzinger’s Ordered Resolution Prover - Archive ouverte HAL Access content directly
Journal Articles Journal of Automated Reasoning Year : 2020

Formalizing Bachmair and Ganzinger’s Ordered Resolution Prover

(1) , (2, 3) , (4) , (3, 5)
1
2
3
4
5

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.
Fichier principal
Vignette du fichier
paper.pdf (267.43 Ko) Télécharger le fichier
Origin : Files produced by the author(s)

Dates and versions

hal-03144467 , version 1 (17-02-2021)

Identifiers

Cite

Anders Schlichtkrull, Jasmin Blanchette, Dmitriy Traytel, Uwe Waldmann. Formalizing Bachmair and Ganzinger’s Ordered Resolution Prover. Journal of Automated Reasoning, 2020, 64 (7), pp.1169-1195. ⟨10.1007/s10817-020-09561-0⟩. ⟨hal-03144467⟩
47 View
85 Download

Altmetric

Share

Gmail Facebook Twitter LinkedIn More