Proving termination of associative commutative rewriting systems by rewriting

Abstract

We propose in this paper a special reduction ordering for proving termination of Associative Commutative (AC in short) rewriting systems. This ordering is based on a transformation of the terms by a rewriting system with rules similar to distributivity. We show this is a reduction ordering which works in the AC case since it is AC- commuting, and which provides an automatizable termination tool, since it is stable by instantiation. Thereafter, we show cases where this ordering fails, and propose an extension of this method to other transformation rules such as endomorphism.