Derivational Complexity of Knuth-Bendix Orders Revisited
Georg MoserProceedings of the 13th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR 2006), Lecture Notes in Computer Science 4246, pp. 75 – 89, 2006.
Abstract
We study the derivational complexity of rewrite systems R compatible with KBO, if the signature of R is infinite. We show that the known bounds on the derivation height are preserved, if R fulfils some mild conditions. This allows us to obtain bounds on the derivational height of non simply terminating TRSs. Furthermore, we re-establish the 2-recursive upper-bound on the derivational complexity of finite rewrite systems R compatible with KBO.
BibTeX
@inproceedings{GM-LPAR06, author = "Georg Moser", title = "Derivational Complexity of Knuth-Bendix Orders Revisited", booktitle = "Proceedings of the 13th International Conference on Logic for Programming, Artificial Intelligence and Reasoning", series = "Lecture Notes in Computer Science", volume = 4246, pages = "75--89", year = 2006 }