Path and decomposition orderings for proving AC-termination

Abstract

Term rewriting provides a simple mechanism that can be applied to reasoning in structures defined by 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. An appropriate reduction relation allows reductions modulo the equations in E. The effective computation with this relation presumes E-termination. We will give an overview and a classification of the well-known methods guaranteeing AC-termination based on the recursive path ordering. Furthermore, we will show that these techniques [called associative path orderings] cannot use quasi-orderings on operators. Above all, this report will deal with some new orderings applicable to AC-theories. We apply a slight extension [the embedding of status] of the concept of the associative path ordering of Gnaedig and Lescanne to several path and decomposition orderings. Since these orderings are stronger than the recursive path ordering, the corresponding orderings restricted to AC-theories are more powerful than the associative path ordering. From a practical point of view these new AC-orderings are more interesting than the associative path ordering because the automatic detection of an admissible precedence for orienting the rules of a given system is much easier.