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 them:
- 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.).
- Removal processors using polynomial interpretations with linear and simple-mixed interpretations on natural and rational domains.
- Removal processors using piecewise polynomial interpretations on convex domains using logic-based model generators as AGES and Mace4.
- Polynomial constraint solving using SAT/SMT and CSP techniques (Multisolver and Barcelogic).
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 6.0.4, released in March 2019. It is remarkable that in the last termination competition (2021), 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.