Abstract

The article 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. One 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
interpretations. Furthermore, this generalization perfectly fits the dependency
pair framework which is implemented in virtually every termination prover
dealing with term rewrite systems. We present two dependency pair processors
for increasing interpretations. The novelty of the second one is that it can be
used to eliminate single edges from the dependency graph.

BibTeX

article{HZAM-AMAI09,
 author      = "Harald Zankl and Aart Middeldorp",
 title       = "Increasing Interpretations",
 journal     = "Annals of Mathematics and Artificial Intelligence",
 volume      = 56,
 number      = 1,
 pages       = "87--108",
 year        = 2009
}