On Deciding Satisfiability by DPLL( $\Gamma+{\mathcal T}$ ) and Unsound Theorem Proving
From MaRDI portal
Publication:5191095
DOI10.1007/978-3-642-02959-2_3zbMath1237.68176OpenAlexW124433265WikidataQ118190441 ScholiaQ118190441MaRDI QIDQ5191095
Christopher Lynch, Maria Paola Bonacina, Leonardo de Moura
Publication date: 28 July 2009
Published in: Automated Deduction – CADE-22 (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/978-3-642-02959-2_3
Lua error in Module:PublicationMSCList at line 37: attempt to index local 'msc_result' (a nil value).
Related Items (8)
Semantically-guided goal-sensitive reasoning: model representation ⋮ Modular Termination and Combinability for Superposition Modulo Counter Arithmetic ⋮ Unifying splitting ⋮ Superposition as a decision procedure for timed automata ⋮ On deciding satisfiability by theorem proving with speculative inferences ⋮ A unifying splitting framework ⋮ Combining Instance Generation and Resolution ⋮ SAT-Inspired Eliminations for Superposition
Uses Software
Cites Work
- A fast algorithm for generating reduced ground rewriting systems from a set of ground equations
- Theory decision by decomposition
- A rewriting approach to satisfiability procedures.
- Automated model building
- Model-based Theory Combination
- Rewrite-Based Satisfiability Procedures for Recursive Data Structures
- Engineering DPLL(T) + Saturation
- Decidability and Undecidability Results for Nelson-Oppen and Rewrite-Based Decision Procedures
- Simplification by Cooperating Decision Procedures
- Presburger arithmetic with unary predicates is Π11 complete
- An algorithm for finding canonical sets of ground rewrite rules in polynomial time
- Abstract canonical inference
- New results on rewrite-based satisfiability procedures
- A Decision Procedure for Monotone Functions over Bounded and Complete Lattices
- Computer Science Logic
- Automated Deduction – CADE-20
- On Variable-inactivity and Polynomial Formula-Satisfiability Procedures
This page was built for publication: On Deciding Satisfiability by DPLL( $\Gamma+{\mathcal T}$ ) and Unsound Theorem Proving
