Unification in the Union of Disjoint Equational Theories: Combining Decision Procedures

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

Franz Baader, K. U. Schulz
Unification in the Union of Disjoint Equational Theories: Combining Decision Procedures
J. Symbolic Computation, 21:211-243, 1996

Details
Bibtex

KurzfassungAbstract
Most of the work on the combination of unification algorithms for the union of disjoint equational theories has been restricted to algorithms that compute finite complete sets of unifiers. Thus the developed combination methods usually cannot be used to combine decision procedures, i.e., algorithms that just decide solvability of unification problems without computing unifiers. In this paper we describe a combination algorithm for decision procedures that works for arbitrary equational theories, provided that solvability of so-called unification problems with constant restrictions---a slight generalization of unification problems with constants---is decidable for these theories. As a consequence of this new method, we can, for example, show that general A-unifiability, i.e., solvability of A-unification problems with free function symbols, is decidable. Here A stands for the equational theory of one associative function symbol. Our method can also be used to combine algorithms that compute finite complete sets of unifiers. Manfred Schmidt-Schau{ss}' combination result, the until now most general result in this direction, can be obtained as a consequence of this fact. We also obtain the new result that unification in the union of disjoint equational theories is finitary, if general unification---i.e., unification of terms with additional free function symbols---is finitary in the single theories.
Forschungsgruppe:Research Group: AutomatentheorieAutomata Theory

@article{ BaaderSchulz-JSC-96,
  author = {F. {Baader} and K. U. {Schulz}},
  journal = {J. Symbolic Computation},
  pages = {211--243},
  title = {Unification in the Union of Disjoint Equational Theories: {C}ombining Decision Procedures},
  volume = {21},
  year = {1996},
}