Tyrolean Termination Tool 2
The Tyrolean Termination Tool 2 (TTT2) is a tool for automatically proving (and disproving) termination of term rewrite systems. It is the completely redesigned successor of TTT.



The current version is 1.20. Get recent versions. Or directly access the mercurial repository for the latest development version.


TTT2 was originally developed by Martin Korp, Christian Sternagel, Harald Zankl, and Aart Middeldorp.
The current developers are Christian Sternagel and Aart Middeldorp.
For any questions or feedback please write to ttt2 at informatik dot uibk dot ac dot at.


Bertram Felgenhauer, Simon Legner, Jonas Schöpf, Sarah Winkler.

Third Party Libraries

TTT2 interfaces the SAT solver MiniSat. Furthermore it relies on CamlIDL.

Tools using TTT2

Some tools which use TTT2 in some form or another

A LaTeX Macro for Typesetting TTT2

In order to refer to our termination tool from your LaTeX-code correctly, please use the following macro:
The result should look approximately as follows