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.
- 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