Polynomial Interpretations with Negative Coecients

Abstract. Polynomial interpretations are a useful technique for proving termination of term rewrite systems. We show how polynomial interpre-tations with negative coecients, like x 1 for a unary function symbol or x y for a binary function symbol, can be used to extend the class of rewrite systems that can be automatically proved terminating.