A Formalization of the SCL(FOL) Calculus: Simple Clause Learning for First-Order Logic (Q7361827)
From MaRDI portal
!
This is the item page for this Wikibase entity, intended for internal use and editing purposes. Please use the normal view instead:
AFP entry Simple_Clause_Learning
| Language | Label | Description | Also known as |
|---|---|---|---|
| default for all languages | No label defined |
||
| English | A Formalization of the SCL(FOL) Calculus: Simple Clause Learning for First-Order Logic |
AFP entry Simple_Clause_Learning |
Statements
20 April 2023
0 references
Martin Desharnais-Schäfer
0 references
A Formalization of the SCL(FOL) Calculus: Simple Clause Learning for First-Order Logic (English)
0 references
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.
0 references
0 references
