Abstract

We study the derivational complexity induced by the (basic) dependency pair
method. Suppose the derivational complexity induced by a termination method is
closed under elementary functions. We show that the derivational complexity
induced by the dependency pair method based on this termination technique is
the same as for the direct technique. Therefore, the derivational complexity
induced by the dependency pair method based on lexicographic path orders or
multiset path orders is multiple recursive or primitive recursive,
respectively. Moreover for the dependency pair method based on Knuth-Bendix
orders, we obtain that the derivational complexity function is majorised by the
Ackermann function. These characterisations are essentially optimal.

BibTeX

@inproceedings{GMAS-RTA09,
author      = "Georg Moser and Andreas Schnabl",
title       = "The Derivational Complexity Induced by the Dependency Pair
               Method",
booktitle   = "Proceedings of the 20th International Conference on Rewriting
               Techniques and Applications",
series      = "Lecture Notes in Computer Science",
volume      = 5595,
pages       = "255--269",
publisher   = "Springer-Verlag",
year        = 2009
}