Innermost Termination of Rewrite Systems by Labeling
René Thiemann and Aart MiddeldorpProceedings of the 7th International Workshop on Reduction Strategies in Rewriting and Programming (WRS 2007), Electronic Notes in Theoretical Computer Science 204, pp. 3 – 19, 2008.
Abstract
Semantic labeling is a powerful transformation technique for
proving termination of term rewrite systems. The semantic
part is given by a model or a quasi-model of the rewrite rules.
A variant of semantic labeling is predictive labeling where the
quasi-model condition is only required for the usable rules.
In this paper we investigate how semantic and predictive labeling can
be used to prove innermost termination. Moreover,
we show how to reduce the set of usable rules for predictive labeling
even further, both in the termination and
the innermost termination case.
BibTeX
@inproceedings{RTAM-WRS07, author = "Ren{\'e} Thiemann and Aart Middeldorp", title = "Innermost Termination of Rewrite Systems by Labeling", booktitle = "Proceedings of the 7th International Workshop on Reduction Strategies in Rewriting and Programming", series = "Electronic Notes in Theoretical Computer Science", volume = 204, pages = "3--19", year = 2008 }
© 2008 Elsevier B.V.