Automatically proving termination where simplification orderings fail

Abstract

To prove termination of term rewriting systems (TRSs), several methods have been developed to synthesize suitable well-founded orderings automatically. However, virtually all orderings that are amenable to automation are so-called simplification orderings. Unfortunately, there exist numerous interesting and relevant TRSs that cannot be oriented by orderings of this restricted class and therefore their termination cannot be proved automatically with the existing techniques.

In this paper we present a new approach which allows to apply the standard techniques for automated termination proofs to those TRSs where these techniques failed up to now. For that purpose we have developed a procedure which, given a TRS, generates a set of inequalities (constraints) automatically. If there exists a well-founded ordering satisfying these constraints, then the TRS is terminating. It turns out that for many TRSs where a direct application of standard techniques fails, these standard techniques can nevertheless synthesize a well-founded ordering satisfying the generated constraints. In this way, termination of numerous (also non-simply terminating) TRSs can be proved fully automatically.

This work was partially supported by the Deutsche Forschungsgemeinschaft under grant no. Wa 652/7-1 as part of the focus program ‘Deduktion’.

These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.