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.

• Type: Conference
• Year: 2004
• Where: AISC
• Authors: Nao Hirokawa, Aart Middeldorp
• Keywords: AISC 2004, Artificial Intelligence, Function Symbol, Polynomial Interpretations, Rewrite Systems