An Isabelle/HOL Formalization of the SCL(FOL) Calculus

DOI10.1007/978-3-031-38499-8_7MaRDI QIDQ6492734zbMATH OpenFDO

Authors Martin Bromberger, Martin Desharnais, Christoph Weidenbach

Publication date 26 April 2024

Copyright license Creative Commons Attribution 4.0 International

Full work available at URL https://doi.org/10.1007/978-3-031-38499-8_7

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Cites work

• A comprehensive framework for saturation theorem proving
• A verified SAT solver framework with learn, forget, restart, and incrementality
• A verified SAT solver framework with learn, forget, restart, and incrementality
• Deciding the Bernays-Schoenfinkel fragment over bounded difference constraints by simple clause learning over theories
• Formalizing Bachmair and Ganzinger's ordered resolution prover
• Formalizing Bachmair and Ganzinger's ordered resolution prover
• Locales: a module system for mathematical theories
• SCL clause learning from simple models
• SCL(EQ): SCL for first-order logic with equality

Cited in

(3)

• A modular formalization of superposition in Isabelle/HOL
• A stepwise refinement proof that SCL(FOL) simulates ground ordered resolution
• First-order automatic literal model generation

This page was built for publication: An Isabelle/HOL Formalization of the SCL(FOL) Calculus

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6492734)