Proving termination properties with mu-term

Abstract

mu-term is a tool which can be used to verify a number of termination properties of (variants of) Term Rewriting Systems (TRSs): termination of rewriting, termination of innermost rewriting, termination of order-sorted rewriting, termination of context-sensitive rewriting, termination of innermost context-sensitive rewriting and termination of rewriting modulo specific axioms. Such termination properties are essential to prove termination of programs in sophisticated rewriting-based programming languages. Specific methods have been developed and implemented in mu-term in order to efficiently deal with most of them. In this paper, we report on these new features of the tool. © 2011 Springer-Verlag Berlin Heidelberg.