TORPA: Termination Of Rewriting Proved Automatically

By this tool proofs of (relative) termination of string rewriting systems (SRS) can be generated automatically. It was developed by Hans Zantema starting in July 2003. It is based on a combination of polynomial and matrix interpretations, recursive path order, semantic labelling, dependency pairs, transformation order, dummy elimination and RFC-match-bounds. Proofs of non-termination are found by using ancestor graphs.

In both the termination competition of 2004 and the termination competition of 2005 this tool performed the best of all tools in the category of string rewriting.

The following versions 1.3 (May 2004), 1.4 (April 2005), 1.5 (February 2006) and 1.6 (May 2006) are available:

A plain version in Pascal. This version accepts the TPDB format as defined for the termination competition . Versions 1.5 and 1.6 also accept plain format.
Source file of TORPA 1.3.
Linux executable of TORPA 1.3.
Source file of TORPA 1.4.
Linux executable of TORPA 1.4.
Source file of TORPA 1.5.
Linux executable of TORPA 1.5.
Source file of TORPA 1.6.
Linux executable of TORPA 1.6.
For instance, if the executable is called torpa16, then by
```
torpa15
(RULES a a b b -> b b b a a a )
```
or even simpler
```
torpa15
aabb -> bbbaaa
```
a termination proof of the single rule aabb -> bbbaaa is generated.
A version with a full graphical user interface, to be run on Windows. This version accepts both the TPDB format and a simpler format also suitable for relative termination. Further documentation is obtained by pressing the HELP button in this program.
Zip file containing Windows executable of TORPA 1.3.
Zip file containing Windows executable of TORPA 1.4.
Zip file containing Windows executable of TORPA 1.5.
Zip file containing Windows executable of TORPA 1.6.

A detailed description of the techniques used in version 1.3 is given in the paper in the Journal of Automated Reasoning.
For more information contact h.zantema@tue.nl.

In the same team two other tools for automatically proving termination have been developed: TPA and TEPARLA.

TPA: Termination Proved Automatically

By this tool proofs of (relative) termination of term rewriting can be generated automatically. It was developed by Adam Koprowski starting in November 2004, as a part of his PhD project. It is based on a combination of polynomial interpretations, recursive path order, and semantic labelling, the latter both by booleans and by natural numbers. For semantic labelling with natural numbers recursive path order was extended to deal with infinite signatures.
The tool is available as a Linux executable.
For more information contact a.koprowski@tue.nl or see the TPA home page.

TEPARLA : TErmination Proved Automatically using Recursive LAbelling

By this tool proofs of (relative) termination of term rewriting can be generated automatically. It was developed by Jeroen van der Wulp between September 2004 and July 2005, as the main result of his master's project. It is based on a combination of polynomial interpretations, recursive path order, and semantic labelling. Here the labelling is only by booleans, but the power of the approach is in using this recursively. For instance, a termination proof of the single rule aabb -> bbbaaa is generated using a five level deep labelling.
The tool is available as a Linux executable.
For more information contact J.v.d.Wulp@tue.nl.

Last update: August 7, 2006