MU-TERM is a tool which can be used to verify a number of termination properties of Term Rewriting Systems 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.
A number of powerful techniques and features have been implemented and combined to achieve such termination proofs automatically. Among others:
- Modular treatment of termination problems at the TRS level.
- Dependency pairs and Context-sensitive dependency pairs (including SCC treatment, narrowings, usable rules, etc).
- RPO and CS-RPO termination.
- Polynomial termination using polynomials with non-negative integer and rational coefficients.
- Polynomial constraint solving using SAT/SMT and CSP techniques.
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.07, released in December 2011. It is remarkable that in the last 'full run' of the TPDB, MU-TERM is the most powerful tool for proving termination of context-sensitive rewriting and the third most powerful tool for proving termination of rewriting.
|
| "Una manera de hacer Europa" |