2008 | OriginalPaper | Chapter
Usable Rules for Context-Sensitive Rewrite Systems
Authors : Raúl Gutiérrez, Salvador Lucas, Xavier Urbain
Published in: Rewriting Techniques and Applications
Publisher: Springer Berlin Heidelberg
Activate our intelligent search to find suitable subject content or patents.
Select sections of text to find matching patents with Artificial Intelligence. powered by
Select sections of text to find additional relevant content using AI-assisted search. powered by
Recently, the dependency pairs (DP) approach has been generalized to context-sensitive rewriting (CSR). Although the
context-sensitive dependency pairs (CS-DP) approach
provides a very good basis for proving termination of CSR, the current developments basically correspond to a ten-years-old DP approach. Thus, the task of adapting all recently introduced dependency pairs techniques to get a more powerful approach becomes an important issue. In this direction,
usable rules
are one of the most interesting and powerful notions. Actually usable rule have been investigated in connection with proofs of
innermost termination
of CSR. However, the existing results apply to a quite restricted class of systems. In this paper, we introduce a notion of usable rules that can be used in proofs of termination of CSR with arbitrary systems. Our benchmarks show that the performance of the CS-DP approach is much better when such usable rules are considered in proofs of termination of CSR.