Proving termination of associative-commutative rewriting systems using the Knuth-Bendix ordering

Abstract

Term rewriting systems provide a simple mechanism for computing in equations. An equation is converted into a directed rewrite rule by comparing both sides w.r.t. an ordering. However, there exist equations which are incomparable. The handling of such equations includes, for example, partitioning the given equational theory into a set R of rules and a set E of equations. The appropriate reduction relation allows reductions modulo the equations in E. The effective computation with this relation presumes E-termination. Classical termination methods cannot directly guarantee E-termination. This report deals with a new ordering applicable to (R,E)-systems where E contains associative-commutative equations. The method is based on the Knuth-Bendix ordering and is AC-commuting, a property introduced by Jouannaud and Munoz.