[Termtools] New MU-TERM site and web interface

[Salvador Lucas]

Dear all,

We are pleased to announce the new web site for the termination tool 
MU-TERM:

  http://zenon.dsic.upv.es/muterm

which includes a web interface for the tool:

  http://zenon.dsic.upv.es/muterm/muterm.php

as well as standalone (graphical and command-line) versions of the tool 
over several platforms (Linux, Mac OS X, Windows).

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

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 and CSP techniques

The application is written in Haskell and has been developed with GHC, a 
popular Haskell compiler. The tool has a graphical user interface using 
the wxHaskell graphics library, and a web interface which has been 
developed using HAppS. 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.

Enjoy!

The MU-TERM team.