The there exists*for all* part of the theory of ground term algebra modulo an AC symbol is undecidable
We show that the There Exists*For All* part of the equational theory modulo an AC symbol is undecidable. This solves the open problem 25 from the RTA list. We show that this result holds also for the equational theory modulo an ACI symbol. (C) 2002 Elsevier Science (USA).
equational theories unification decidability