SCL(FOL) Can Simulate Non-Redundant Superposition Clause Learning

DOI10.1007/978-3-031-38499-8_8MaRDI QIDQ6492736zbMATH OpenFDO

Authors Martin Bromberger, 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_8

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) 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 comprehensive framework for saturation theorem proving
• An efficient subsumption test pipeline for BS(LRA) clauses
• Deciding the Bernays-Schoenfinkel fragment over bounded difference constraints by simple clause learning over theories
• Faster, higher, stronger: E 2.3
• Formalizing Bachmair and Ganzinger's ordered resolution prover
• Inst-Gen -- a modular approach to instantiation-based automated reasoning
• Paramodulation-based theorem proving
• Resolution theorem proving
• Rewrite-based Equational Theorem Proving with Selection and Simplification
• SCL clause learning from simple models
• SCL(EQ): SCL for first-order logic with equality
• iProver – An Instantiation-Based Theorem Prover for First-Order Logic (System Description)

Cited in

(2)

• Automatic bit- and memory-precise verification of eBPF code
• A stepwise refinement proof that SCL(FOL) simulates ground ordered resolution

This page was built for publication: SCL(FOL) Can Simulate Non-Redundant Superposition Clause Learning

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