This Isabelle/HOL formalization covers the unexecutable specification of Simple Clause Learning for first-order logic without equality: SCL(FOL). The main results are formal proofs of soundness, non-redundancy of learned clauses, termination, and refutational completeness. Compared to the unformalized version, the formalized calculus is simpler, a number of results were generalized, and the non-redundancy statement was strengthened. We found and corrected one bug in a previously published version of the SCL Backtrack rule. Compared to related formalizations, we introduce a new technique for showing termination based on non-redundant clause learning.
- First-Order Terms
- A Verified Functional Implementation of Bachmair and Ganzinger’s Ordered Resolution Prover
- Formalization of Bachmair and Ganzinger’s Ordered Resolution Prover
- A Comprehensive Framework for Saturation Theorem Proving
- Extensions to the Comprehensive Framework for Saturation Theorem Proving