Theory decision by decomposition
From MaRDI portal
Publication:1041591
DOI10.1016/j.jsc.2008.10.008zbMath1192.68626OpenAlexW1980250820MaRDI QIDQ1041591
Maria Paola Bonacina, Mnacho Echenim
Publication date: 3 December 2009
Published in: Journal of Symbolic Computation (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1016/j.jsc.2008.10.008
superpositioncombination of theoriesautomated theorem proving: rewritingsatisfiability modulo theories: decision procedures
Lua error in Module:PublicationMSCList at line 37: attempt to index local 'msc_result' (a nil value).
Related Items (9)
Modular Termination and Combinability for Superposition Modulo Counter Arithmetic ⋮ Quantifier-Free Equational Logic and Prime Implicate Generation ⋮ On First-Order Model-Based Reasoning ⋮ On deciding satisfiability by theorem proving with speculative inferences ⋮ An instantiation scheme for satisfiability modulo theories ⋮ Semantically-guided goal-sensitive reasoning: inference system and completeness ⋮ Canonical Ground Horn Theories ⋮ On Deciding Satisfiability by DPLL( $\Gamma+{\mathcal T}$ ) and Unsound Theorem Proving ⋮ SMELS: satisfiability modulo equality with lazy superposition
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- M\textbf{ath}SAT: Tight integration of SAT and mathematical decision procedures
- A rewriting approach to satisfiability procedures.
- Modular proof systems for partial functions with Evans equality
- Efficient theory combination via Boolean search
- Decision procedures for extensions of the theory of arrays
- Automated model building
- Rewrite-Based Decision Procedures
- Model-based Theory Combination
- Rewrite-Based Satisfiability Procedures for Recursive Data Structures
- Solving SAT and SAT Modulo Theories
- Architecting Solvers for SAT Modulo Theories: Nelson-Oppen with DPLL
- SMELS: Satisfiability Modulo Equality with Lazy Superposition
- Engineering DPLL(T) + Saturation
- Simplify: a theorem prover for program checking
- Solving Quantified Verification Conditions Using Satisfiability Modulo Theories
- Efficient E-Matching for SMT Solvers
- ${\mathcal{T}}$ -Decision by Decomposition
- Automatic Decidability and Combinability Revisited
- Decidability and Undecidability Results for Nelson-Oppen and Rewrite-Based Decision Procedures
- Simplification by Cooperating Decision Procedures
- Proving Theorems with the Modification Method
- Applying Light-Weight Theorem Proving to Debugging and Verifying Pointer Programs
- Lazy abstraction
- New results on rewrite-based satisfiability procedures
- Splitting on Demand in SAT Modulo Theories
- Automatic Combinability of Rewriting-Based Satisfiability Procedures
- Automated Deduction – CADE-20
- On Variable-inactivity and Polynomial Formula-Satisfiability Procedures
- Using First-Order Theorem Provers in the Jahob Data Structure Verification System
- Frontiers of Combining Systems
- Frontiers of Combining Systems
- A Computing Procedure for Quantification Theory
- A machine program for theorem-proving
- Theory and Applications of Satisfiability Testing
- Computer Aided Verification
- Processor verification using efficient reductions of the logic of uninterpreted functions to propositional logic
- Verification, Model Checking, and Abstract Interpretation
This page was built for publication: Theory decision by decomposition
