Vade-mecum of Polynomial Orderings

Abstract

Orderings on polynomial interpretations of operators represent a powerful technique for proving the termination of rewrite systems. We discuss most of the well-known features concerning this method including heuristics for the generation of adequate interpretations orienting a given system, strategies for deciding the positiveness of a polynomial, restricted interpretations to guarantee E-termination and some improvements [such as the Cartesian product of polynomials]. This report is a detailed source of examples that illustrate the uncertainties of polynomial orderings. Furthermore, we develop new aspects involving two approaches that are suitable to simple implementations, a few suggestions for producing adequate interpretations [e.g., a technique for automatically generating linear polynomials], some new orderings handling underlying theories, a new improved version of polynomial orderings [based on the Knuth-Bendix ordering with status] as well as a detailed comparison of the various approaches together with path and decomposition orderings. Thus, the report in hand is a kind of vade-mecum of most of the known as well as new results concerned with polynomial orderings.