Termination Proofs in the Dependency Pair Framework May Induce Multiple Recursive Derivational Complexity
Logic in Computer Science
2011-03-29 v1
Abstract
We study the derivational complexity of rewrite systems whose termination is provable in the dependency pair framework using the processors for reduction pairs, dependency graphs, or the subterm criterion. We show that the derivational complexity of such systems is bounded by a multiple recursive function, provided the derivational complexity induced by the employed base techniques is at most multiple recursive. Moreover we show that this upper bound is tight.
Cite
@article{arxiv.1103.5082,
title = {Termination Proofs in the Dependency Pair Framework May Induce Multiple Recursive Derivational Complexity},
author = {Georg Moser and Andreas Schnabl},
journal= {arXiv preprint arXiv:1103.5082},
year = {2011}
}
Comments
22 pages, extended conference version