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.
BibTeX:
<![CDATA[
@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"}
]]></plaintext></p></div></div>