An algorithm for finding canonical sets of ground rewrite rules in polynomial time
Jean H. Gallier, Paliath Narendran, David A. Plaisted, Stan Raatz, Wayne Snyder · Journal of the ACM · 1993
In this paper, it is shown that there is an algorithm that, given by finite set E of ground equations, produces a reduced canonical rewriting system R equivalent to E in polynomial time. This algorithm based on congruence closure performs simplification steps guided by a total simplification ordering on ground terms, and it runs in time O(n 3 ) .