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. 175184, 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. 249268, 2004
ps.gz
pdf

Polynomial Interpretations with Negative
Coefficients
Proc. of the 7th International Conference on Artificial
Intelligence and Symbolic Computation,
LNAI 3249, pp. 185198, 2004
ps.gz
pdf

Automating the Dependency Pair Method
Information and Computation 199(1,2), pp. 172199, 2005
ps.gz
pdf
The Tyrolean Termination Tool is the successor of the awardwinning
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. 311320, 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 firstorder rewrite systems, it
can handle simplytyped applicative
rewrite systems. Such systems are transformed into ordinary
firstorder rewrite systems by the transformation described in the
following paper:

Takahito Aoto and Toshiyuki Yamada
Termination of SimplyTyped Applicative
TRSs
Proc. of the 2nd International Workshop on HigherOrder Rewriting,
Technical Report AIB200403, RWTH Aachen, pp. 6165, 2004
ps.gz