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
and Hans Zantema.
Matchbox/Poly takes part in the
Termination Competition 2009
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
- (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:
- (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
- 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:
You may be interested in other automated termination provers:
(Of course there are more. I only listed those I know
that implement match bounds and/or have an online interface.)
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.)
(for string rewriting systems) by Hans Zantema, TU Eindhoven