System description: an equational constraints solver

摘要

Equational formulae are first-order formulae containing only "=" as a predicate symbol. A substitution #delta# is a solution of an equational formula F iff F #sigma# is valid in the finite tree algebra (i.e. when = is interpreted as the syntactic equality on the Herbrand universe). Equational formulae have many applications in the domains of Automated Deduction, Artificial Intelligence and Computer Science (Program verification, negation in logic programming [5,13,3], inductive proofs [6], model building [4,1,19] etc.). They have been studied by many authors for several years. In particular, the validity problem for equational formulae in the empty theory has been proven to be decidable [15,12,14,9].