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 TORPA performed the best of all tools in the category of string rewriting.

More recently (2013-2015), based on TORPA, the tool TORPAcyc has been developed for proving termination of cycle rewriting.

The following versions are available:

Zip file containing TORPAcyc for proving termination of cycle rewriting. It contains the source code and a LINUX executable, the external tool Yices, several examples and a file README containing instructions. (2015)
A paper describing the underlying techniques, appeared at RTA/TLCA2014.
A web interface developed by David Sabel for torpacyc and its combination with a transformational approach described in a paper on this transformational approach .
A plain version of TORPA in Pascal. This version accepts the TPDB format as defined for the termination competition .
Source file of TORPA 1.3. (2004)
Linux executable of TORPA 1.3.
Source file of TORPA 1.4. (2005)
Linux executable of TORPA 1.4.
Source file of TORPA 1.5. (2006)
Linux executable of TORPA 1.5.
Source file of TORPA 1.6. (2006)
Linux executable of TORPA 1.6.
For instance, if the executable is called torpa16, then by
```
torpa16
(RULES a a b b -> b b b a a a )
```
or even simpler
```
torpa16
aabb -> bbbaaa
```
a termination proof of the single rule aabb -> bbbaaa is generated.
A version of TORPA with a full graphical user interface, to be run on Windows. 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 TORPA, version 1.3 is given in the paper in the Journal of Automated Reasoning.
For more information contact h.zantema@tue.nl.

Last update: January, 2015