mu-term: A Tool for Proving Termination of Context-Sensitive Rewriting

S Lucas - International Conference on Rewriting Techniques and …, 2004 - Springer
International Conference on Rewriting Techniques and Applications, 2004Springer
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 …
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.
Springer
以上显示的是最相近的搜索结果。 查看全部搜索结果