Termination of Associative-Commutative Rewriting by Dependency Pairs

Claude Marché and Xavier Urbain


A new criterion for termination of rewriting has been described by Arts and Giesl in 1997. We show how this criterion can be generalised to rewriting modulo associativity and commutativity. We also show how one can build weak AC-compatible reduction orderings which may be used in this criterion.

preliminary version