Raúl Gutiérrez

[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.

[download] 

Download in PDF format.

[BibTeX entry] 

@inproceedings{aef+08,
    author = {Alarc\'on, B. and Emmes, F. and 
              Fuhs, C. and Giesl, J. and 
              Guti\'errez, R. and Lucas, S. and
              Schneider-Kamp, P. and Thiemann, R.},
    title = {{Improving Context-Sensitive Dependency 
              Pairs}},
    booktitle = {Proc.\ of the 15th International 
                 Conference on Logic for Programming, 
                 Artificial Intelligence and
                 Reasoning, LPAR'08},
    year = {2008},
    editor = {Cervesato, I. and Veith, H. and 
              Voronkov, A.},
    pages = {636--651},
    series = {LNCS},
    volume = {5330},
    publisher = {Springer-Verlag}
 }