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:

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

Last update: January, 2015