Abstract

The paper at hand introduces a refinement of interpretation based
termination criteria for term rewrite systems in the dependency
pair setting. Traditional methods share the property that—in
order to be successful—all rewrite rules must (weakly) decrease
with respect to some measure. The novelty of our approach is that
we allow some rules to increase the interpreted value. These rules
are found by simultaneously searching for adequate polynomial
interpretations while considering the information of the dependency
graph. We prove that our method extends the termination proving power
of linear natural interpretations. Furthermore, this generalization
perfectly fits the recursive SCC decomposition algorithm which is
implemented in virtually every termination prover dealing with term
rewrite systems.

BibTeX

@inproceedings{HZAM-AISC08,
  author      = "Harald Zankl and Aart Middeldorp",
  title       = "Increasing Interpretations",
  booktitle   = "Proceedings of the 9th International Conference on
                 Artificial Intelligence and Symbolic Computation",
  series      = "Lecture Notes in Artificial Intelligence",
  volume      = 5144,
  pages       = "191--205",
  publisher   = "Springer-Verlag",
  year        = 2008
}