An Algorithm for Finding Canonical Sets of Ground Rewrite Rules in Polynomial Time

Abstract

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 O1993. © 1993, ACM. All rights reserved.