Proving Termination Properties with mu-term

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.

• Type: Journal
• Year: 2010
• Where: AMAST
• Authors: Beatriz Alarcón, Raúl Gutiérrez, Salvador Lucas, Rafael Navarro-Marset
• Keywords: AMAST 2010, Context-sensitive Rewriting, Innermost Context-sensitive Rewriting, Software Engineering, Termination Properties