Abstract
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.
License
Topics
Session Ordered_Resolution_Prover
- Map2
- Lazy_List_Liminf
- Lazy_List_Chain
- Clausal_Logic
- Herbrand_Interpretation
- Abstract_Substitution
- Inference_System
- Ground_Resolution_Model
- Unordered_Ground_Resolution
- Ordered_Ground_Resolution
- Proving_Process
- Standard_Redundancy
- FO_Ordered_Resolution
- FO_Ordered_Resolution_Prover
Depends on
Used by
- A Modular Formalization of Superposition
- A Formalization of the SCL(FOL) Calculus: Simple Clause Learning for First-Order Logic
- Extensions to the Comprehensive Framework for Saturation Theorem Proving
- A Formal Proof of The Chandy–Lamport Distributed Snapshot Algorithm
- A Comprehensive Framework for Saturation Theorem Proving
- A Verified Functional Implementation of Bachmair and Ganzinger’s Ordered Resolution Prover