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.
Keywords Dependency pairs - term rewriting - termination
Work partially supported by the EU (FEDER) and the Spanish MEC, under grants TIN 2004-7943-C04-02, TIN 2007-68118-C02 and
HA 2006-0007.