Formalizing Bachmair and Ganzinger's Ordered Resolution Prover

Publikation: Bidrag til tidsskriftTidsskriftartikelfagfællebedømt

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.
OriginalsprogEngelsk
TidsskriftJournal of Automated Reasoning
Vol/bind64
Sider (fra-til)1169–1195
ISSN0168-7433
DOI
StatusUdgivet - 2020
Eksternt udgivetJa

ID: 245667075