Abstract
We study the derivational complexity of rewrite systems \(\mathcal{R}\) compatible with KBO, if the signature of \(\mathcal{R}\) is infinite. We show that the known bounds on the derivation height are preserved, if \(\mathcal{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 \(\mathcal{R}\) compatible with KBO.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Terese: Term Rewriting Systems. In: Cambridge Tracks in Theoretical Computer Science, vol. 55. Cambridge University Press, Cambridge (2003)
Hirokawa, N., Middeldorp, A.: Tyrolean termination tool. In: Giesl, J. (ed.) RTA 2005. LNCS, vol. 3467, pp. 175–184. Springer, Heidelberg (2005)
Giesl, J., Thiemann, R., Schneider-Kamp, P., Falke, S.: Automated termination proofs with Aprove. In: van Oostrom, V. (ed.) RTA 2004. LNCS, vol. 3091, pp. 210–220. Springer, Heidelberg (2004)
Zantema, H.: Termination of string rewriting proved automatically. J. Automated Reasoning 34, 105–109 (2005)
Koprowski, A.: TPA: Termination Proved Automatically (System Description). In: Pfenning, F. (ed.) RTA 2006. LNCS, vol. 4098, pp. 257–266. Springer, Heidelberg (2006)
Koprowski, A., Zantema, H.: Automation of Recursive Path Ordering for Infinite Labelled Rewrite Systems. In: Furbach, U., Shankar, N. (eds.) IJCAR 2006. LNCS, vol. 4130, pp. 332–346. Springer, Heidelberg (2006)
Hofbauer, D., Lautemann, C.: Termination proofs and the length of derivations. In: RTA 1989. LNCS, vol. 355, pp. 167–177. Springer, Heidelberg (1989)
Hofbauer, D.: Termination Proofs and Derivation Lengths in Term Rewriting Systems. PhD thesis, Technische Universität Berlin (1991)
Hofbauer, D.: Termination proofs by multiset path orderings imply primitive recursive derivation lengths. Theor. Comput. Sci. 105, 129–140 (1992)
Weiermann, A.: Termination proofs for term rewriting systems with lexicographic path ordering imply multiply recursive derivation lengths. Theor. Comput. Sci. 139, 355–362 (1995)
Lepper, I.: Derivation lengths and order types of Knuth-Bendix order. Theor. Comput. Sci. 269, 433–450 (2001)
Bachmair, L.: Proof methods for equational theories. PhD thesis, University of Illionois (1987)
Zantema, H.: Termination of term rewriting by semantic labelling. Fundamenta Informaticae 24, 89–105 (1995)
Jech, T.: Set Theory. Springer, Heidelberg (2002)
Martin, U.: How to chose weights in the Knuth-Bendix ordering. In: Lescanne, P. (ed.) RTA 1987. LNCS, vol. 256, pp. 42–53. Springer, Heidelberg (1987)
Dershowitz, N.: Termination of Rewriting. J. Symbolic Computation (1987)
Korovin, K., Voronkov, A.: Orienting rewrite rules with the Knuth-Bendix order. Information and Compuation 183, 165–186 (2003)
Rose, H.: Subrecursion: Functions and Hierarchies. Oxford University Press, Oxford (1984)
Moser, G., Weiermann, A.: Relating derivation lengths with the slow-growing hierarchy directly. In: Nieuwenhuis, R. (ed.) RTA 2003. LNCS, vol. 2706, pp. 296–310. Springer, Heidelberg (2003)
Hofbauer, D.: Termination proofs by context-dependent interpretations. In: Middeldorp, A. (ed.) RTA 2001. LNCS, vol. 2051, pp. 108–121. Springer, Heidelberg (2001)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2006 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Moser, G. (2006). Derivational Complexity of Knuth-Bendix Orders Revisited. In: Hermann, M., Voronkov, A. (eds) Logic for Programming, Artificial Intelligence, and Reasoning. LPAR 2006. Lecture Notes in Computer Science(), vol 4246. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11916277_6
Download citation
DOI: https://doi.org/10.1007/11916277_6
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-48281-9
Online ISBN: 978-3-540-48282-6
eBook Packages: Computer ScienceComputer Science (R0)