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.).
  • 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.


Union Europea   Ministerio de Economía y Competitividad   Ministerio de ciencia e innovación

Generalitat Valenciana   Universitat Politècnica de València   DSIC

“Una manera de hacer Europa”