A note on a canonical theory with undecidable unification and matching problem (Q1098623)

This research note gives a simple proof of the fact that the unification and matching problem is undecidable in the class of equational theories that can be embedded into a canonical term rewriting system. We present a canonical term rewriting system for integer arithmetic and show that the unification and matching problem in the corresponding equational theory is equivalent to Hilbert's tenth problem which is well known to be undecidable.