# Combination Techniques and Decision Problems for Disunification Combination Techniques and Decision Problems for Disunification
Theoretical Computer Science B, 142:229-255, 1995
• KurzfassungAbstract
Previous work on combination techniques considered the question of how to combine unification algorithms for disjoint equational theories \$E_1,ldots,E_n\$ in order to obtain a unification algorithm for the union \$E_1 cup ldotscup E_n\$ 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 ldotscup E_n\$. Our first result says that solvability of disunification problems in the free algebra of the combined theory \$E_1 cup ldotscup E_n\$ is decidable if solvability of disunification problems with linear constant restrictions in the free algebras of the theories \$E_i\$ (\$i = 1,ldots,n\$) is decidable. In order to decide ground solvability (i.e., solvability in the initial algebra) of disunification problems in \$E_1 cup ldotscup E_n\$ we have to consider a new kind of subproblem for the particular theories \$E_i\$, namely solvability (in the free algebra) of disunification problems with linear constant restriction under the additional constraint that values of variables are not \$E_i\$-equivalent to variables. The correspondence between ground solvability and this new kind of solvability holds, {em (1)} if one theory \$E_i\$ is the free theory with at least one function symbol and one constant, or {em (2)} if the initial algebras of all theories \$E_i\$ 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.
• Forschungsgruppe:Research Group: Automatentheorie
```@article{ BaaderSchulz-TCS-95,
author = {F. {Baader} and K.U. {Schulz}},
journal = {Theoretical Computer Science B},
pages = {229--255},
title = {Combination Techniques and Decision Problems for Disunification},
volume = {142},
year = {1995},
}
```