An Isabelle/HOL Formalization of the SCL(FOL) Calculus
From MaRDI portal
Publication:6492734
DOI10.1007/978-3-031-38499-8_7MaRDI QIDQ6492734
Martin Bromberger, Martin Desharnais, Christoph Weidenbach
Publication date: 26 April 2024
Mechanization of proofs and logical operations (03B35) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)
Cites Work
- A verified SAT solver framework with learn, forget, restart, and incrementality
- SCL(EQ): SCL for first-order logic with equality
- Deciding the Bernays-Schoenfinkel fragment over bounded difference constraints by simple clause learning over theories
- SCL clause learning from simple models
- Locales: a module system for mathematical theories
- A Verified SAT Solver Framework with Learn, Forget, Restart, and Incrementality
- Formalizing Bachmair and Ganzinger's ordered resolution prover
- Formalizing Bachmair and Ganzinger's ordered resolution prover
- A comprehensive framework for saturation theorem proving
This page was built for publication: An Isabelle/HOL Formalization of the SCL(FOL) Calculus