MOVES Seminar, 22 May 2009, 11:00

Fabian Emmes

 

Improving Context-Sensitive Dependency Pairs

  

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.