Term rewriting and the completion of term rewriting systems are important tools for deciding equational problems in such fields as automated deduction, algebraic specification, and discrete mathematics. Probably the most infuriating limitation of the basic rewriting framework is its inability to deal with commutative operators: commutativity cannot be turned into a terminating rewrite rule. Rewriting modulo a set of equations avoids this problem by taking such problematic rules out of the rewriting process and moving them into the set of equations. In practice, one often works modulo AC, which axiomatizes associativity and commutativity. Rewriting modulo AC does not come for free: completion requires AC unification instead of syntactic unification, which increases the complexity considerably. If the associative-commutative operators satisfy additional equations, one may be tempted to add these equations to AC if unification in the extended theory is less complex. Unfortunately, in the existing frameworks for completion modulo E, this is often not possible, since they impose strong restrictions on E; for example, they need an E-compatible reduction order (which does not exist for all E).

The author introduces normalized rewriting as a way out of this dilemma. Before rewriting modulo AC, the terms are normalized with respect to a fixed set of rules S. In this setting, it is sufficient to have an AC-compatible reduction order, but completion may use unification in any theory between AC and AC ∪ S. This paper provides a completion algorithm for normalized rewriting, and shows that it outperforms completion modulo AC for several important algebraic theories. In addition, it proves old and new decidability results for ground equations modulo various interesting theories. The paper is well written, but the details of the proofs will probably be comprehensible only to readers familiar with the techniques used (such as proof orders à la Bachmair).