The undecidability of the unification and matching problem for canonical theories (Q1077931)

The problem whether there exists a unifying substitution for two terms is considered in the class of theories which can be embedded into canonical term rewriting systems. The problem is shown to be undecidable, even if we restrict the substitutions to matching ones. This implies that the class of admissible canonical theories is a proper subset of the class of canonical theories.