Improving Context-Sensitive Dependency Pairs

Beatriz Alarcón, Fabian Emmes, Carsten Fuhs, Jürgen Giesl, Raúl Gutiérrez, Salvador Lucas, Peter Schneider-Kamp, and René Thiemann

Proceedings of the 15th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR 2008), Lecture Notes in Artificial Intelligence 5330, pp. 636 – 651, 2008.


Context-sensitive dependency pairs (CS-DPs) are currently the most powerful method for automated termination analysis of context-sensitive rewriting. However, compared to DPs for ordinary rewriting, CS-DPs suffer from two main drawbacks: (a) CS-DPs can be collapsing. This complicates the handling of CS-DPs and makes them less powerful in practice. (b) There does not exist a “DP framework” for CS-DPs which would allow one to apply them in a flexible and modular way. This paper solves drawback (a) by introducing a new definition of CS-DPs. With our definition, CS-DPs are always non-collapsing and thus, they can be handled like ordinary DPs. This allows us to solve drawback (b) as well, i.e., we extend the existing DP framework for ordinary DPs to context-sensitive rewriting. We implemented our results in the tool AProVE and successfully evaluated them on a large collection of examples.


  PDF |    doi:10.1007/978-3-540-89439-1_44  |  © Springer


author = "Beatriz Alarc{\"o}n and Fabian Emmes and Carsten Fuhs and J{\"u}rgen Giesl and
Ra{\'u}l Guti{\'e}rrez and Salvador Lucas and Peter Schneider-Kamp and
Ren{\'e} Thiemann",
title = "Improving Context-Sensitive Dependency Pairs",
booktitle = "Proceedings of the 15th International Conferences on Logic for
Programming, Artificial Intelligence and Reasoning",
series = "Lecture Notes in Artificial Intelligence",
volume = 5330,
publisher = "Springer-Verlag",
year = 2008,
pages = "636--651"
Nach oben scrollen