Context-Sensitive Dependency Pairs

Termination is one of the most interesting problems when dealing with context-sensitive rewrite systems. Although there is a good number of techniques for proving termination of context-sensitive rewriting (CSR), the dependency pair approach, one of the most powerful techniques for proving termination of rewriting, has not been investigated in connection with proofs of termination of CSR. In this paper, we show how to use dependency pairs in proofs of termination of CSR. The implementation and practical use of the developed techniques yield a novel and powerful framework which improves the current state-of-the-art of methods for proving termination of CSR.

• Type: Conference
• Year: 2006
• Where: FSTTCS
• Authors: Beatriz Alarcón, Raúl Gutiérrez, Salvador Lucas
• Keywords: Context-sensitive Rewrite Systems, Dependency Pair Approach, Dependency Pairs, FSTTCS 2006, Software Engineering