On deciding confluence of finite string-rewriting systems modulo partial commutativity

AbstractThe theory of confluent and coherent equational term-rewriting systems is carried over to string-rewriting systems on partially commutative alphabets. It is shown that it is decidable whether or not a finite E-terminating string-rewriting system R on alphabet Σ is R,E-convergent, where E denotes the congruence induced by a partial commutativity relation C on Σ. The main part of the paper gives a proof that a finite E-terminating string-rewriting system R is R,E-convergent if and only if certain minimal critical pairs are F-confluent, respectively E-coherent