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.

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"
}