Abstract

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.

BibTeX Entry

@inproceedings{HM-AISC04,
 author    = "Nao Hirokawa and Aart Middeldorp",
 title     = "Polynomial Interpretations with Negative Coefficients",
 booktitle = "Proceedings of the 7th International Conference on
              Artificial Intelligence and Symbolic Mathematical
              Computation",
 series    = "Lecture Notes in Artificial Intelligence",
 volume    = 3249,
 pages     = "185--198",
 year      = 2004,
 doi       = "10.1007/978-3-540-30210-0\_16"
}