Abstract

We study the complexity of rewrite systems shown terminating via the
dependency pair framework using processors for reduction pairs, dependency
graphs, or the subterm criterion. The complexity of such systems is
bounded by a multiple recursive function, provided the complexity induced
by the employed base techniques is at most multiple recursive. Moreover
this upper bound is tight.

BibTeX

@inproceedings{GMAS-RTA11,
  author    = "Georg Moser and Andreas Schnabl",
  title     = "Termination Proofs in the Dependency Pair Framework May
               Induce Multiple Recursive Derivational Complexity",
  booktitle = "Proceedings of the 22nd International Conference on Rewriting
               Techniques and Applications",
  series    = "Leibniz International Proceedings in Informatics",
  volume    = 10,
  pages     = "235--250",
  year      = 2011
}