Congruences Generated by Extended Ground Term Rewrite Systems
Sándor Vágvölgyi · Fundamenta Informaticae · 2009
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.