Model-based Theory Combination
From MaRDI portal
Publication:2864402
DOI10.1016/j.entcs.2008.04.079zbMath1277.03007OpenAlexW2110780548MaRDI QIDQ2864402
Nikolaj Bjørner, Leonardo de Moura
Publication date: 6 December 2013
Published in: Electronic Notes in Theoretical Computer Science (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1016/j.entcs.2008.04.079
Lua error in Module:PublicationMSCList at line 37: attempt to index local 'msc_result' (a nil value).
Related Items (19)
Decision Procedures for Region Logic ⋮ Conflict-driven satisfiability for theory combination: lemmas, modules, and proofs ⋮ Sharing Is Caring: Combination of Theories ⋮ Satisfiability Modulo Theories ⋮ Generalized arrays for Stainless frames ⋮ An SMT-based approach to weak controllability for disjunctive temporal problems with uncertainty ⋮ Adapting Real Quantifier Elimination Methods for Conflict Set Computation ⋮ Combining decision procedures by (model-)equality propagation ⋮ On deciding satisfiability by theorem proving with speculative inferences ⋮ Being careful about theory combination ⋮ On Interpolation in Decision Procedures ⋮ Combining Decision Procedures by (Model-)Equality Propagation ⋮ On Deciding Satisfiability by DPLL( $\Gamma+{\mathcal T}$ ) and Unsound Theorem Proving ⋮ Ground Interpolation for Combined Theories ⋮ Sets with Cardinality Constraints in Satisfiability Modulo Theories ⋮ Delayed theory combination vs. Nelson-Oppen for satisfiability modulo theories: a comparative analysis ⋮ Theory decision by decomposition ⋮ A posthumous contribution by Larry Wos: excerpts from an unpublished column ⋮ On interpolation in automated theorem proving
Uses Software
Cites Work
- Fast congruence closure and extensions
- Complexity, convexity and combinations of theories
- Efficient theory combination via Boolean search
- Solvable cases of the decision problem
- Solving SAT and SAT Modulo Theories
- Simplify: a theorem prover for program checking
- Deciding Combinations of Theories
- Simplification by Cooperating Decision Procedures
- Computer Aided Verification
- Delayed Theory Combination vs. Nelson-Oppen for Satisfiability Modulo Theories: A Comparative Analysis
- To Ackermann-ize or Not to Ackermann-ize? On Efficiently Handling Uninterpreted Function Symbols in $\mathit{SMT}(\mathcal{EUF} \cup \mathcal{T})$
This page was built for publication: Model-based Theory Combination
