MU-TERM is a tool which can be used to verify a number of termination properties of term rewriting systems (TRSs) via different reduction relations which can be associated to
- termination of rewriting,
- termination of innermost rewriting,
- termination of context-sensitive rewriting,
- termination of innermost context-sensitive rewriting,
- termination of order-sorted rewriting,
- termination of equational rewriting for AvC-theories,
- operational termination of conditional rewriting.
A number of powerful techniques, frameworks and processors have been implemented and combined to achieve such termination proofs automatically. Among others:
- modular treatment of TRSs.
- mechanization of the process of finding a proof of termination by using the appropriate instance of the dependency pair framework (including processors for the SCC treatment, narrowing, instantiation, subterm criterion, reduction pairs with usable rules, RPOs, etc.).
- Polynomial termination using domains with polynomials with non-negative integer and rational coefficients.
- Polynomial termination using convex domains and convex matrix interpretations.
- Polynomial constraint solving using SAT/SMT and CSP techniques (Multisolver).
The application is written in Haskell and has been developed with GHC, a popular Haskell compiler. The web interface is intended to provide a simplified use of the tool and the techniques which can be useful for teaching purposes (for instance, we provide direct access to RPO, polynomial and DP-termination proofs which can be conveniently parameterized).
The current version of MU-TERM is 5.18, released in August 2016. It is remarkable that in the last termination competition (2016), MU-TERM participated in five categories and it is the most powerful tool for proving termination of context-sensitive rewriting and operational termination of conditional rewriting.