Formalizing Bachmair and Ganzinger’s Ordered Resolution Prover

Anders Schlichtkrull, Jasmin Blanchette, Dmitriy Traytel, Uwe Waldmann

Research output: Chapter in Book/Report/Conference proceedingArticle in proceedingsResearchpeer-review

195 Downloads (Pure)

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
Volume10900
PublisherSpringer
Publication date2018
Pages89-107
ISBN (Print)9783319942049
DOIs
Publication statusPublished - 2018
Event9th International Joint Conference on Automated Reasoning - Oxford, United Kingdom
Duration: 14 Jul 201817 Jul 2018

Conference

Conference9th International Joint Conference on Automated Reasoning
CountryUnited Kingdom
CityOxford
Period14/07/201817/07/2018
SeriesLecture Notes in Computer Science
Volume10900
ISSN0302-9743

Fingerprint Dive into the research topics of 'Formalizing Bachmair and Ganzinger’s Ordered Resolution Prover'. Together they form a unique fingerprint.

Cite this