A stepwise refinement proof that SCL(FOL) simulates ground ordered resolution

DOI10.1007/978-3-031-99984-0_17MaRDI QIDQ6869946zbMATH OpenFDO

Authors Martin Bromberger, Martin Desharnais, Christoph Weidenbach

Publication date 21 January 2026

Copyright license Creative Commons Attribution 4.0 International

Full work available at URL https://doi.org/10.1007/978-3-031-99984-0_17

zbMATH Keywords

interactive theorem provingordered resolutionSCL(ground) first-order logicnon-redundant clause learning

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Formalization of mathematics in connection with theorem provers (68V20) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Cites work

• scientific article; zbMATH DE number 3299786 (Why is no real title available?)
• A formally verified compiler back-end
• A modular formalization of superposition in Isabelle/HOL
• An Isabelle/HOL Formalization of the SCL(FOL) Calculus
• Deciding the Bernays-Schoenfinkel fragment over bounded difference constraints by simple clause learning over theories
• Formalizing Bachmair and Ganzinger's ordered resolution prover
• Principles and practice of constraint programming -- CP '96. Second international conference, CP '96, Cambridge, MA, USA, August 19--22, 1996. Proceedings
• Rewrite-based Equational Theorem Proving with Selection and Simplification
• SCL clause learning from simple models
• SCL(EQ): SCL for first-order logic with equality
• SCL(FOL) Can Simulate Non-Redundant Superposition Clause Learning

This page was built for publication: A stepwise refinement proof that SCL(FOL) simulates ground ordered resolution

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