TY - JOUR
T1 - Generalizing DPLL and satisfiability for equalities
AU - Badban, Baharen
AU - van de Pol, Jaco
AU - Tveretina, Olga
AU - Zantema, Hans
PY - 2007/8
Y1 - 2007/8
N2 - 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
AB - 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
U2 - 10.1016/j.ic.2007.03.003
DO - 10.1016/j.ic.2007.03.003
M3 - Article
VL - 205
SP - 1188
EP - 1211
JO - Information and Computation
JF - Information and Computation
IS - 8
ER -