Búsqueda avanzada

The 2D Dependency Pair Framework for conditional rewrite systems (Trabajo ya publicado)


Different termination properties of conditional term rewriting systems have been recently described emphasizing the bidimensional nature of the termination behavior of conditional rewriting. The absence of infinite sequences of rewriting steps (termination in the usual sense), provides the horizontal dimension. The absence of infinitely many attempts to launch the subsidiary processes that are required to check the rule’s condition and perform a single rewriting step has been called V-termination and provides the vertical dimension. We have characterized these properties by means of appropriate notions of dependency pairs and dependency chains. In this paper we introduce a 2D Dependency Pair Framework for automatically proving and disproving all these termination properties. Our implementation of the framework as part of the termination tool MU-TERM and the benchmarks obtained so far suggest that the 2D Dependency Pair Framework is currently the most powerful technique for proving operational termination of conditional term rewriting systems.

Palabras Clave:

Conditional term rewriting - dependency pairs - Operational Termination - Program analysis





Este artículo tiene una licencia de uso CreativeCommons - Reconocimiento (by)

Descarga el artículo haciendo click aquí.

Ver la referencia en formato Bibtex