cl-banner

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

Georg Moser and Andreas Schnabl

Proceedings of the 22nd International Conference on Rewriting Techniques and Applications (RTA 2011), Leibniz International Proceedings in Informatics 10, pp. 235 – 250, 2011.

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.

 

  PDF |    doi:10.4230/LIPIcs.RTA.2011.235  |  © Creative Commons License – NC – ND

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
}
Nach oben scrollen