Sciweavers

Share
CORR
2011
Springer

Termination Proofs in the Dependency Pair Framework May Induce Multiple Recursive Derivational Complexity

8 years 5 days ago
Termination Proofs in the Dependency Pair Framework May Induce Multiple Recursive Derivational Complexity
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. 1998 ACM Subject Classification F.2.2, F.4.1, D.2.4, D.2.8 Keywords and phrases Complexity, DP Framework, Multiple Recursive Functions
Georg Moser, Andreas Schnabl
Added 16 May 2011
Updated 16 May 2011
Type Journal
Year 2011
Where CORR
Authors Georg Moser, Andreas Schnabl
Comments (0)
books