cl-banner

The Derivational Complexity Induced by the Dependency Pair Method

Georg Moser and Andreas Schnabl

Proceedings of the 20th International Conference on Rewriting Techniques and Applications (RTA 2009), Lecture Notes in Computer Science 5595, pp. 255 – 269, 2009.

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.

 

  PDF |    doi:10.1007/978-3-642-02348-4_18  |  © Springer

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