Combination techniques and decision problems for disunification

Abstract

Previous work on combination techniques considered the question of how to combine unification algorithms for disjoint equational theories E_{1} ,...,E_{n} in order to obtain a unification algorithm for the union E1 unified ... unified En of the theories. Here we want to show that variants of this method may be used to decide solvability and ground solvability of disunification problems in E_{1}cup...cup E_{n}. Our first result says that solvability of disunification problems in the free algebra of the combined theory E_{1}cup...cup E_{n} is decidable if solvability of disunification problems with linear constant restrictions in the free algebras of the theories E_{i}(i = 1,...,n) is decidable. In order to decide ground solvability (i.e., solvability in the initial algebra) of disunification problems in E_{1}cup...cup E_{n} we have to consider a new kind of subproblem for the particular theories Ei, namely solvability (in the free algebra) of disunification problems with linear constant restriction under the additional constraint that values of variables are not Ei-equivalent to variables. The correspondence between ground solvability and this new kind of solvability holds, (1) if one theory Ei is the free theory with at least one function symbol and one constant, or (2) if the initial algebras of all theories Ei are infinite. Our results can be used to show that the existential fragment of the theory of the (ground) term algebra modulo associativity of a finite number of function symbols is decidable; the same result follows for function symbols which are associative and commutative, or associative, commutative and idempotent.