Polynomial Interpretations with Negative Coefficients

Polynomial interpretations are a useful technique for proving termination of term rewrite systems. We show how polynomial interpretations with negative coefficients, 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.Proceedings of the 7th International Conference, AISC 2004, Linz, Austria, September 22-24, 2004