Description

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:

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.


Union Europea   
Generalitat Valenciana   Universitat Politècnica de València   DSIC
“Una manera de hacer Europa”