cl-banner

Proving Quadratic Derivational Complexities using Context Dependent Interpretations

Georg Moser and Andreas Schnabl

Proceedings of the 19th International Conference on Rewriting Techniques and Applications (RTA 2008), Lecture Notes in Computer Science 5117, pp. 276 – 290, 2008.

Abstract

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.

 

  PDF |    doi:10.1007/978-3-540-70590-1_19  |  © Springer

BibTeX 

@inproceedings{GMAS-RTA08,
author = "Georg Moser and Andreas Schnabl",
title = "Proving Quadratic Derivational Complexities using Context Dependent Interpretations",
booktitle = "Proceedings of the 19th International Conference on Rewriting
Techniques and Applications",
series = "Lecture Notes in Computer Science",
volume = 5117,
publisher = "Springer-Verlag",
year = 2008,
pages = "276--290"
}
Nach oben scrollen