### Abstract

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.

### License

BSD License

### Topics

- Logic/General logic/Mechanization of proofs

### Session Simple_Clause_Learning

- Abstract_Renaming_Apart
- Ordered_Resolution_Prover_Extra
- SCL_FOL
- Correct_Termination
- Trail_Induced_Ordering
- Initial_Literals_Generalize_Learned_Literals
- Multiset_Order_Extra
- Non_Redundancy
- Wellfounded_Extra
- Termination
- Completeness
- Invariants

### Depends on

- 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

## Cite

×

Simple_Clause_Learning-AFP

    @article{Simple_Clause_Learning-AFP,
      author  = {Martin Desharnais},
      title   = {A Formalization of the SCL(FOL) Calculus: Simple Clause Learning for First-Order Logic},
      journal = {Archive of Formal Proofs},
      month   = {April},
      year    = {2023},
      note    = {\url{https://isa-afp.org/entries/Simple_Clause_Learning.html},
                 Formal proof development},
      ISSN    = {2150-914x},
    }

Download

## Download

× Download latest

Older releases:

- Sep 13, 2023 : Isabelle2023
- Apr 22, 2023 : Isabelle2022