Generalizing DPLL and satisfiability for equalities


Badban, Bahareh and Pol, Jaco van de and Tveretina, Olga and Zantema, Hans (2007) Generalizing DPLL and satisfiability for equalities. Information and computation, 205 (8). pp. 1188-1211. ISSN 0890-5401

[img] PDF
Restricted to UT campus only
: Request a copy
Abstract:We present GDPLL, a generalization of the DPLL procedure. It solves the satisfiability problem for decidable fragments of quantifier-free first-order logic. Sufficient conditions are identified for proving soundness, termination and completeness of GDPLL. We show how the original DPLL procedure is an instance. Subsequently the GDPLL instances for equality logic, and the logic of equality over infinite ground term algebras are presented. Based on this, we implemented a decision procedure for inductive datatypes. We provide some new benchmarks, in order to compare variants.
Item Type:Article
Copyright:© 2007 Elsevier
Electrical Engineering, Mathematics and Computer Science (EEMCS)
Research Group:
Link to this item:
Official URL:
Export this item as:BibTeX
HTML Citation
Reference Manager


Repository Staff Only: item control page

Metis ID: 242016