Context-Sensitive Dependency Pairs?

Abstract. 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 rewrit-ing (CSR), the dependency pair approach, one of the most powerful tech-niques 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 im-plementation 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