Advertisement
Published in:
2009 | OriginalPaper | Chapter
The Derivational Complexity Induced by the Dependency Pair Method
Authors : Georg Moser, Andreas Schnabl
Published in: Rewriting Techniques and Applications
Publisher: Springer Berlin Heidelberg
Activate our intelligent search to find suitable subject content or patents.
Select sections of text to find matching patents with Artificial Intelligence. powered by
Select sections of text to find additional relevant content using AI-assisted search. powered by
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.