T y r o l e a n T e r m i n a t i o n T o o l

The Tyrolean Termination Tool is a tool for automatically proving termination of rewrite systems based on the dependency pair method of Arts and Giesl. It is described in the following paper by Nao Hirokawa and Aart Middeldorp:

Tyrolean Termination Tool
Proc. of the 16th International Conference on Rewriting Techniques and Applications, LNCS 3467, pp. 175-184, 2005
ps.gz pdf

The proof techniques used in the tool are described in the following papers (by the same authors):

Dependency Pairs Revisited
Proc. of the 15th International Conference on Rewriting Techniques and Applications, LNCS 3091, pp. 249-268, 2004
ps.gz pdf
Polynomial Interpretations with Negative Coefficients
Proc. of the 7th International Conference on Artificial Intelligence and Symbolic Computation, LNAI 3249, pp. 185-198, 2004
ps.gz pdf
Automating the Dependency Pair Method
Information and Computation 199(1,2), pp. 172-199, 2005
ps.gz pdf

The Tyrolean Termination Tool is the successor of the award-winning Tsukuba Termination Tool, which is described in the following paper:

Tsukuba Termination Tool
Proc. of the 14th International Conference on Rewriting Techniques and Applications, LNCS 2706, pp. 311-320, 2003
ps.gz pdf errata

The Tyrolean Termination Tool is not only much faster and more powerful than its predecessor, it also is has a more convenient user interface. Furthermore, in addition to ordinary first-order rewrite systems, it can handle simply-typed applicative rewrite systems. Such systems are transformed into ordinary first-order rewrite systems by the transformation described in the following paper:

Takahito Aoto and Toshiyuki Yamada
Termination of Simply-Typed Applicative TRSs
Proc. of the 2nd International Workshop on Higher-Order Rewriting, Technical Report AIB-2004-03, RWTH Aachen, pp. 61-65, 2004
ps.gz