Combining Matching Algorithms: The Regular Case

Tobias Nipkow

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.


@article{Nipkow-JSC-91, author="Tobias Nipkow", title="Combining Matching Algorithms: The Regular Case", journal="Journal of Symbolic Computation",volume=12,number=6, year=1991,pages="633--653"}