Deciding confluence of certain term rewriting systems in polynomial time
Ashish Tiwari · 2003
We present a polynomial time algorithm for deciding confluence of ground term rewrite systems. We generalize the decision procedure to get a polynomial time algorithm, assuming that the maximum arity of a symbol in the signature is a constant, for deciding confluence of rewrite systems where each rule contains a shallow linear term on one side and a ground term on the other. The existence of a polynomial time algorithm for deciding confluence of ground rewrite systems was open for a long time and was independently solved only recently. Our decision procedure is based on the concepts of abstract congruence closure and abstract rewrite closure.