Combining matching algorithms: The regular case

The problem of combining matching algorithms for equational theories with disjoint signatures is studied. It is shown that the combined matching problem is in general undecidable but that it becomes decidable if all theories are regular. For the case of regular theories an efficient combination algorithm is developed. As part of that development we present a simple algorithm for solving the word problem in the combination of arbitrary equational theories with disjoint signatures