Abstract
We describe and discuss DPLL(T), a parametric calculus for proving the satisfiability of ground formulas in a logical theory T. The calculus tightly integrates a decision procedure for the satisfiability in T of sets of literals into a sequent calculus based on the well-known method by Davis, Putman, Logemann and Loveland for proving the satisfiability of propositional formulas. For being based on the DPLL method, DPLL(T) can incorporate a number of very effective search heuristics developed by the SAT community for that method. Hence, it can be used as the formal basis for novel and efficient implementations of satisfiability checkers for theories with decidable ground consequences. © 2002 Springer-Verlag.
Cite
CITATION STYLE
Tinelli, C. (2002). A DPLL-based calculus for ground satisfiability modulo theories. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 2424 LNAI, pp. 308–319). Springer Verlag. https://doi.org/10.1007/3-540-45757-7_26
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
