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

Authors Georg Moser, Andreas Schnabl



PDF
Thumbnail PDF

File

LIPIcs.RTA.2011.235.pdf
  • Filesize: 0.55 MB
  • 16 pages

Document Identifiers

Author Details

Georg Moser
Andreas Schnabl

Cite AsGet BibTex

Georg Moser and Andreas Schnabl. Termination Proofs in the Dependency Pair Framework May Induce Multiple Recursive Derivational Complexity. In 22nd International Conference on Rewriting Techniques and Applications (RTA'11). Leibniz International Proceedings in Informatics (LIPIcs), Volume 10, pp. 235-250, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2011)
https://doi.org/10.4230/LIPIcs.RTA.2011.235

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.
Keywords
  • Complexity
  • DP Framework
  • Multiple Recursive Functions

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail