Email Gateway (Apr 22 2023 at 03:25): Email Gateway (Apr 22 2023 at 03:25):From: Tobias Nipkow <nipkow@in.tum.de>
A Formalization of the SCL(FOL) Calculus: Simple Clause Learning for First-Order
Logic
Martin Desharnais
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.
https://www.isa-afp.org/entries/Simple_Clause_Learning.html
Enjoy!
Last updated: Apr 23 2024 at 08:19 UTC