Tyrolean Termination Tool 2

Description

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.

Download

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

News

Contact

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.

Contributors

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:
\newcommand\TTTT{%
 \textsf{T\kern-0.15em\raisebox{-0.55ex}T\kern-0.15emT\kern-0.15em\raisebox{-0.55ex}2}%
}
The result should look approximately as follows