Generalizing DPLL and satisfiability for equalities

Share/Save/Bookmark

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
214kB
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
Faculty:
Electrical Engineering, Mathematics and Computer Science (EEMCS)
Research Group:
Link to this item:http://purl.utwente.nl/publications/61974
Official URL:http://dx.doi.org/10.1016/j.ic.2007.03.003
Export this item as:BibTeX
EndNote
HTML Citation
Reference Manager

 

Repository Staff Only: item control page

Metis ID: 242016