Formalization of Bachmair and Ganzinger's Ordered Resolution Prover

Publication: Research - peer-reviewJournal article – Annual report year: 2018

Documents

View graph of relations

This Isabelle/HOL formalization covers Sections 2 to 4 of Bachmair and Ganzinger’s “Resolution Theorem Proving” chapter in the Handbook of Automated Reasoning. This includes soundness and completeness of unordered and ordered variants of ground resolution with and without literal selection, the standard redundancy criterion, a general framework for refutational theorem proving, and soundness and completeness of an abstract first-order prover.
Original languageEnglish
Book seriesArchive of Formal Proofs
Number of pages117
ISSN2150-914X
StatePublished - 2018

Bibliographical note

https://www.isa-afp.org/entries/Ordered_Resolution_Prover.html

Download as:
Download as PDF
Select render style:
APAAuthorCBE/CSEHarvardMLAStandardVancouverShortLong
PDF
Download as HTML
Select render style:
APAAuthorCBE/CSEHarvardMLAStandardVancouverShortLong
HTML
Download as Word
Select render style:
APAAuthorCBE/CSEHarvardMLAStandardVancouverShortLong
Word

Download statistics

No data available

ID: 145948642