Termination of Associative-Commutative Rewriting by Dependency Pairs
Claude Marché and Xavier Urbain
Abstract
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