MU-TERM: a tool for proving termination of rewriting with replacement restrictions

Author

Salvador Lucas

Abstract

This paper describes MU-TERM, a tool which can be used to automatically prove termination of computational restrictions of rewriting such as context-sensitive rewriting and lazy rewriting. The tool can also be used to prove termination of rewriting. In this sense, MU-TERM provides the first implementation of reduction orderings based on polynomial interpretations over the rational numbers.