×

zbMATH — the first resource for mathematics

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].

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.)
Software:
Chaff
PDF BibTeX XML Cite
Full Text: DOI