Congruences Generated by Extended Ground Term Rewrite Systems
We show that it is decidable for any extended ground term rewrite system R whether there is a ground term rewrite system S such that the congrunce  (R)* generated by R is equal to the congruence  (S)* generated by S. If the answer is yes, then we can effectively construct such a ground term rewrite system S. We characterize congruences generated by extended ground term rewrite systems.
extended ground term rewrite system tree automaton