Matchbox: Weighted Automata for Analysing Termination and Complexity of Rewriting

This is the web page for the program Matchbox that implements word and tree automata algorithms for Rewriting with Height Annotations and Matrix Interpretations as described in the papers by Jörg Endrullis, Alfons Geser, Dieter Hofbauer, Adam Koprowski, Johannes Waldmann, and Hans Zantema.

Matchbox/Poly takes part in the Termination Competition 2009 in the Complexity of Rewriting Category.

Here is a List of Methods that Matchbox uses in termination proofs (2008 version).

Here you can use Matchbox (not the most current version, sorry) online for:

trivia: The name Matchbox comes from one special kind of annotation called match height that we use for string rewriting. For term rewriting, there are top heights and roof heights as well.

What's new:

(14. 12. 09) Matchbox/Poly computes complexity information. It can read the xml input format.
(12. 2. 08) Matchbox now has arctic matrix interpretations for TRS ... and it boldly goes below zero ... and it outputs (Rainbow) certificates.
(25. 5. 07) Matchbox takes part in the Termination Competition 2007. This time, we only do termination of string rewriting (standard and relative). New methods are: arctic matrix interpretations and compressed loops.
(12. 6. 06) Matchbox takes part in the Termination Competition 2006
(30. 4. 06) Andreas Gebhardt built an online interface to several termination provers and a database of hard problems: http://autotool.imn.htwk-leipzig.de:8080/websrs/
(10. 3. 06) added CGI interface for matrix method
(May 05) Jörg Endrullis has developed a much more efficient algorithm to compute compatible automata and verify match bounds for string rewriting. See his termination prover Jambox.
the (minor) differences from 2004 to 2005 in Matchbox itself are:
- for SRS: additional method relative RFC match bounds
- for TRS: additional state splitting transformation

Useful information on Matchbox:

Some of the papers on theoretical background are available from the authors' pages: Alfons Geser, Dieter Hofbauer.
Matchbox System description paper (published in RTA04) (ps |pdf )
Matchbox took part in both the SRS and TRS divisions of the Termination Competition in 2004 and 2005.
Module interface documentation: (haddock)
Source code: http://141.57.11.163/cgi-bin/cvsweb/box/
Download Matchbox executable (for GNU Linux on i*86 architecture): download/
Alternatively, download and build Matchbox from source: Installation guide

You may be interested in other automated termination provers:

AProVE Lehr- und Foschungsgruppe Informatik II, RWTH Aachen.
(Web site includes Java Applet.)
Tyrolean (was: Tsukuba) Termiation Tool by Nao Hirokawa and Aart Middeldorp, Innsbruck.
(Web site includes CGI interface.)
TORPA (for string rewriting systems) by Hans Zantema, TU Eindhoven

(Of course there are more. I only listed those I know that implement match bounds and/or have an online interface.)

http://www.imn.htwk-leipzig.de/~waldmann/