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é ThiemannProceedings 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.
Abstract
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.
BibTeX
@inproceedings{BAFECFJGRGSLPSKRT-LPAR08,
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"
}