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

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)

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)