Solving satisfiability of ground term algebras using DPLL and unification

B. Badban; J.C. Pol, van de; O. Tveretina; H. Zantema

Solving satisfiability of ground term algebras using DPLL and unification

B. Badban, J.C. Pol, van de, O. Tveretina, H. Zantema

Formal System Analysis

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Academic

2 Downloads (Pure)

Abstract

Abstract datatypes can be viewed as sorted ground term algebras. Unification can be used to solve conjunctions of equations. We give a new algorithm to extend this to the full quantifier free fragment, i.e. including formulas with disjunction and negation. The algorithm is based on unification (to deal with equality) and DPLL (to deal with propositional logic). In this paper we present our algorithm as an instance of a generalized DPLL algorithm. We prove soundness and completeness of the class of generalized DPLL algorithms, in particular for the algorithm for ground term algebras.

Original language	English
Title of host publication	Proceedings 18th Workshop on Unification (UNIF2004, Cork, Ireland, July 5, 2004; affiliated with IJCAR'04)
Editors	M. Kohlhase
Publication status	Published - 2004

Cite this

@inproceedings{60aae9e82b4c407b85256a63caf593e6,

title = "Solving satisfiability of ground term algebras using DPLL and unification",

abstract = "Abstract datatypes can be viewed as sorted ground term algebras. Unification can be used to solve conjunctions of equations. We give a new algorithm to extend this to the full quantifier free fragment, i.e. including formulas with disjunction and negation. The algorithm is based on unification (to deal with equality) and DPLL (to deal with propositional logic). In this paper we present our algorithm as an instance of a generalized DPLL algorithm. We prove soundness and completeness of the class of generalized DPLL algorithms, in particular for the algorithm for ground term algebras.",

author = "B. Badban and {Pol, van de}, J.C. and O. Tveretina and H. Zantema",

year = "2004",

language = "English",

editor = "M. Kohlhase",

booktitle = "Proceedings 18th Workshop on Unification (UNIF2004, Cork, Ireland, July 5, 2004; affiliated with IJCAR'04)",

}

TY - GEN

T1 - Solving satisfiability of ground term algebras using DPLL and unification

AU - Badban, B.

AU - Pol, van de, J.C.

AU - Tveretina, O.

AU - Zantema, H.

PY - 2004

Y1 - 2004

N2 - Abstract datatypes can be viewed as sorted ground term algebras. Unification can be used to solve conjunctions of equations. We give a new algorithm to extend this to the full quantifier free fragment, i.e. including formulas with disjunction and negation. The algorithm is based on unification (to deal with equality) and DPLL (to deal with propositional logic). In this paper we present our algorithm as an instance of a generalized DPLL algorithm. We prove soundness and completeness of the class of generalized DPLL algorithms, in particular for the algorithm for ground term algebras.

AB - Abstract datatypes can be viewed as sorted ground term algebras. Unification can be used to solve conjunctions of equations. We give a new algorithm to extend this to the full quantifier free fragment, i.e. including formulas with disjunction and negation. The algorithm is based on unification (to deal with equality) and DPLL (to deal with propositional logic). In this paper we present our algorithm as an instance of a generalized DPLL algorithm. We prove soundness and completeness of the class of generalized DPLL algorithms, in particular for the algorithm for ground term algebras.

M3 - Conference contribution

BT - Proceedings 18th Workshop on Unification (UNIF2004, Cork, Ireland, July 5, 2004; affiliated with IJCAR'04)

A2 - Kohlhase, M.

ER -

Solving satisfiability of ground term algebras using DPLL and unification

Abstract

Fingerprint

Cite this