Abstract

This paper presents an in and lasy decision procedure for the first-order equality theory over a Herbrand universe as well as for that of rational trees. The procedure is based on a conjunctive normal form and consists of two algorithms, one algorithm to decide satisfiability and one for transforming a universally quantified negated constraint into a new constraint in normal form. We will also show that a general formula in either theory can be rewritten into an equivalent normal form, thus providing a general decision procedure. The normal form and the design of the decision procedure have been chosen to meet the requirements of a concurrent constraint programming language.