The Word Problem of ACD-Ground theories is Undecidable


We prove that there exists an ACD-ground theory, an equational theory defined by a set of ground equations plus the associativity and commutativity of two binary symbols * and +, and the distributivity of * over +, for which the word problem is undecidable.

full paper