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. Current (non-)termination techniques include: approximated dependency graph, argument filtering, bounds, dependency pair method, Knuth-Bendix order, lexicographic path order, loop detection, matrix interpretation, polynomial interpretation, predictive labeling, recursive SCC, root-labeling, semantic labeling, simple projection and subterm criterion, uncurrying, and usable rules.


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



The main authors are Martin Korp, Christian Sternagel, Harald Zankl, and Aart Middeldorp.
For any questions or feedback please write to ttt2 at informatik dot uibk dot ac dot at.

Third Party Libraries

TTT2 interfaces the SAT solver MiniSat and the SMT solver Yices. 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