A model-constructing satisfiability calculus. (English) Zbl 1426.68251
Giacobazzi, Roberto (ed.) et al., Verification, model checking, and abstract interpretation. 14th international conference, VMCAI 2013, Rome, Italy, January 20–22, 2013. Proceedings. Berlin: Springer. Lect. Notes Comput. Sci. 7737, 1-12 (2013).
Summary: 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.
For the entire collection see [Zbl 1298.68027].
For the entire collection see [Zbl 1298.68027].
MSC:
| 68T20 | Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) |
| 03B10 | Classical first-order logic |
| 03B70 | Logic in computer science |
| 68Q60 | Specification and verification (program logics, model checking, etc.) |
| 68V15 | Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) |
