SCL(FOL) Can Simulate Non-Redundant Superposition Clause Learning
From MaRDI portal
Publication:6492736
DOI10.1007/978-3-031-38499-8_8MaRDI QIDQ6492736
Christoph Weidenbach, Author name not available (Why is that?), Martin Bromberger
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
- Title not available (Why is that?)
- An efficient subsumption test pipeline for BS(LRA) clauses
- 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
- Faster, higher, stronger: E 2.3
- Resolution theorem proving
- Paramodulation-based theorem proving
- iProver – An Instantiation-Based Theorem Prover for First-Order Logic (System Description)
- Rewrite-based Equational Theorem Proving with Selection and Simplification
- Inst-Gen – A Modular Approach to Instantiation-Based Automated Reasoning
- Formalizing Bachmair and Ganzinger's ordered resolution prover
- A comprehensive framework for saturation theorem proving
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)
