We present a new calculus where recent model-based decision procedures and techniques can be justified and combined with the standard DPLL(T) approach to satisfiability modulo theories. The new calculus generalizes the ideas found in CDCL-style propositional SAT solvers to the first-order setting. © Springer-Verlag 2013.
CITATION STYLE
De Moura, L., & Jovanović, D. (2013). A model-constructing satisfiability calculus. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 7737 LNCS, pp. 1–12). Springer Verlag. https://doi.org/10.1007/978-3-642-35873-9_1
Mendeley helps you to discover research relevant for your work.