Generalizing DPLL and satisfiability for equalities

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

Research output: Contribution to journalArticleAcademicpeer-review

7 Citations (Scopus)
2 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 languageEnglish
Pages (from-to)1188-1211
Number of pages24
JournalInformation and computation
Volume205
Issue numberLNCS4549/8
DOIs
Publication statusPublished - Aug 2007

Fingerprint

Algebra
Equality
Logic
Satisfiability Problem
Decision Procedures
Quantifiers
Soundness
First-order Logic
Termination
Completeness
Fragment
Benchmark
Sufficient Conditions
Term
Generalization

Keywords

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

Cite this

Badban, Bahareh ; van de Pol, Jan Cornelis ; Tveretina, Olga ; Zantema, Hans. / Generalizing DPLL and satisfiability for equalities. In: Information and computation. 2007 ; Vol. 205, No. LNCS4549/8. pp. 1188-1211.
@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 = "8",
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",

}

Generalizing DPLL and satisfiability for equalities. / Badban, Bahareh; van de Pol, Jan Cornelis; Tveretina, Olga; Zantema, Hans.

In: Information and computation, Vol. 205, No. LNCS4549/8, 08.2007, p. 1188-1211.

Research output: Contribution to journalArticleAcademicpeer-review

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

VL - 205

SP - 1188

EP - 1211

JO - Information and computation

JF - Information and computation

SN - 0890-5401

IS - LNCS4549/8

ER -