zbMATH — the first resource for mathematics

Abstract DPLL and abstract DPLL modulo theories. (English) Zbl 1109.68097
Baader, Franz (ed.) et al., Logic for programming, artificial intelligence, and reasoning. 11th international conference, LPAR 2004, Montevideo, Uruguay, March 14–18, 2005. Proceedings. Berlin: Springer (ISBN 3-540-25236-3/pbk). Lecture Notes in Computer Science 3452. Lecture Notes in Artificial Intelligence, 36-50 (2005).
Summary: We introduce Abstract DPLL, a general and simple abstract rule-based formulation of the Davis-Putnam-Logemann-Loveland (DPLL) procedure. Its properties, such as soundness, completeness or termination, immediately carry over to the modern DPLL implementations with features such as non-chronological backtracking or clause learning. This allows one to formally reason about practical DPLL algorithms in a simple way. In the second part of this paper we extend the framework to Abstract DPLL modulo theories. This allows us to express-and formally reason about-state-of-the-art concrete DPLL-based techniques for satisfiability modulo background theories, such as the different lazy approaches, or our DPLL(T) framework.
For the entire collection see [Zbl 1070.68001].

68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)
03B35 Mechanization of proofs and logical operations
BerkMin; Chaff; SATO
Full Text: DOI