MU-TERM: A Tool for Proving Termination of Context-Sensitive Rewriting

Author

Salvador Lucas

Abstract

Restrictions of rewriting can eventually achieve termination by pruning all infinite rewrite sequences issued from every term. Context-sensitive rewriting (CSR) is an example of such a restriction. In CSR, the replacements in some arguments of the function symbols are permanently forbidden. This paper describes MU-TERM, a tool which can be used to automatically prove termination of CSR. The tool implements the generation of the appropriate orderings for proving termination of CSR by means of polynomial interpretations over the rational numbers. In fact, MU-TERM is the first termination tool which generates term orderings based on such polynomial interpretations. These orderings can also be used, in a number of different ways, for proving termination of ordinary rewriting. Proofs of termination of CSR are also possible via existing transformations to TRSs (without any replacement restriction) which are also implemented in MU-TERM.