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

@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,
  publisher   = "Springer-Verlag",
  year        = 2004,
  pages       = "185--198"
}