Combination Techniques and Decision Problems for Disunification

Franz BaaderFranz Baader, K.U. SchulzK.U. Schulz

Franz Baader, K.U. Schulz
Combination Techniques and Decision Problems for Disunification
Theoretical Computer Science B, 142:229-255, 1995

Details
Bibtex

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: AutomatentheorieAutomata Theory

@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},
}