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
}