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. 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.

Download

The current version is 1.11. Get recent versions.

News

• Mar 21 2013: Version 1.10 released (improved compilation for FreeBSD)
• Feb 4 2013: Version 1.09 released
• May 25 2012: Version 1.08 released (PicoSat binding added)
• May 2 2011: Version 1.07 released (using new build system)
• Sep 10 2010: Version 1.05 released. It is now possible to parse DP problems from *.trs files (a DP uses ->t instead of ->).
• May 20 2010: Version 1.04 released (to compile with ocaml 3.11.2)
• March 12 2010: Version 1.03 released (needed for MiniSmt)
• Jan 1 2010: The sources of version 1.02 are now available. This version contains several new techniques such as match-bounds, root-labeling, subterm-criterion, and improved dependency graphs.
• Jul 05 2009: System description is available. © Springer-Verlag.
• Jun 25 2009: The sources of version 1.0 are now available. A version containing match-bounds, root-labeling, and subterm-criterion is under preparation. These methods have been available in older versions.

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.

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

• CaT (Complexity and Termination)
• MkbTT (Multi Completion with Termination Tools)
• TcT (Tyrolean Complexity Tool)

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.2em\raisebox{-0.3em}T\kern-0.2emT\kern-0.2em\raisebox{-0.3em}2}%
}

The result should look approximately as follows