In this paper we study context dependent interpretations, a semantic termination method extending interpretations over the natural numbers, introduced by Hofbauer. We present two subclasses of context dependent interpretations and establish tight upper bounds on the induced derivational complexities. In particular we delineate a class of interpretations that induces quadratic derivational complexity. Furthermore, we present an algorithm for mechanically proving termination of rewrite systems with context dependent interpretations. This algorithm has been implemented and we present ample numerical data for the assessment of the viability of the method. © 2008 Springer-Verlag.
CITATION STYLE
Moser, G., & Schnabl, A. (2008). Proving quadratic derivational complexities using context dependent interpretations. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 5117 LNCS, pp. 276–290). https://doi.org/10.1007/978-3-540-70590-1_19
Mendeley helps you to discover research relevant for your work.