SCL clause learning from simple models
From MaRDI portal
Publication:2305416
DOI10.1007/978-3-030-29436-6_14OpenAlexW2969435376MaRDI QIDQ2305416
Christoph Weidenbach, Alberto Fiori
Publication date: 10 March 2020
Full work available at URL: https://hal.inria.fr/hal-02405550/file/cade27.pdf
Mechanization of proofs and logical operations (03B35) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)
Related Items (9)
A Datalog hammer for supervisor verification conditions modulo simple linear arithmetic ⋮ Semantically-guided goal-sensitive reasoning: decision procedures and the Koala prover ⋮ Deciding the Bernays-Schoenfinkel fragment over bounded difference constraints by simple clause learning over theories ⋮ SCL(EQ): SCL for first-order logic with equality ⋮ SGGS decision procedures ⋮ A posthumous contribution by Larry Wos: excerpts from an unpublished column ⋮ An efficient subsumption test pipeline for BS(LRA) clauses ⋮ SCL(EQ): SCL for first-order logic with equality ⋮ SAT-Inspired Eliminations for Superposition
Cites Work
- Unnamed Item
- Semantically-guided goal-sensitive reasoning: model representation
- Deciding effectively propositional logic using DPLL and substitution sets
- Complete problems in the first-order predicate calculus
- Complexity results for classes of quantificational formulas
- The CADE-14 ATP system competition
- Non-cyclic Sorts for First-Order Satisfiability
- NRCL - A Model Building Approach to the Bernays-Schönfinkel Fragment
- First-Order Logic Theorem Proving and Model Building via Approximation and Instantiation
- Linear Integer Arithmetic Revisited
- Solving SAT and SAT Modulo Theories
- Proof Systems for Effectively Propositional Logic
- Superposition for Bounded Domains
- Inst-Gen – A Modular Approach to Instantiation-Based Automated Reasoning
- Lemma Learning in the Model Evolution Calculus
- Model Representation over Finite and Infinite Signatures
This page was built for publication: SCL clause learning from simple models
