Generalizing DPLL and satisfiability for equalities

Bahareh Badban; Jan Cornelis van de Pol; Olga Tveretina; Hans Zantema

doi:10.1016/j.ic.2007.03.003

Generalizing DPLL and satisfiability for equalities

Bahareh Badban
, Jan Cornelis van de Pol
, Olga Tveretina
, Hans Zantema

Research output: Contribution to journal › Article › Academic › peer-review

7 Citations (Scopus)

202 Downloads (Pure)

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.

Original language	English
Pages (from-to)	1188-1211
Number of pages	24
Journal	Information and computation
Volume	205
Issue number	LNCS4549/8
DOIs	https://doi.org/10.1016/j.ic.2007.03.003
Publication status	Published - Aug 2007

Keywords

DPLL procedure
Decision procedure
Inductive datatypes
Ground term algebra
Satisfiability
EWI-11281
CR-I.2.3
Equality

Access to Document

10.1016/j.ic.2007.03.003

sdarticle-2Final published version, 209 KB

Cite this

@article{7186eca4114c44c8aa2e8a9bce581265,

title = "Generalizing DPLL and satisfiability for equalities",

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.",

keywords = "DPLL procedure, Decision procedure, Inductive datatypes, Ground term algebra, Satisfiability, EWI-11281, CR-I.2.3, Equality",

author = "Bahareh Badban and \{van de Pol\}, \{Jan Cornelis\} and Olga Tveretina and Hans Zantema",

year = "2007",

month = aug,

doi = "10.1016/j.ic.2007.03.003",

language = "English",

volume = "205",

pages = "1188--1211",

journal = "Information and computation",

issn = "0890-5401",

publisher = "Elsevier",

number = "LNCS4549/8",

}

TY - JOUR

T1 - Generalizing DPLL and satisfiability for equalities

AU - Badban, Bahareh

AU - van de Pol, Jan Cornelis

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.

KW - DPLL procedure

KW - Decision procedure

KW - Inductive datatypes

KW - Ground term algebra

KW - Satisfiability

KW - EWI-11281

KW - CR-I.2.3

KW - Equality

U2 - 10.1016/j.ic.2007.03.003

DO - 10.1016/j.ic.2007.03.003

M3 - Article

SN - 0890-5401

VL - 205

SP - 1188

EP - 1211

JO - Information and computation

JF - Information and computation

IS - LNCS4549/8

ER -

Generalizing DPLL and satisfiability for equalities

Abstract

Keywords

Access to Document

Fingerprint

Cite this