News
- Apr 29 2020: Version 1.20 released (maximal polynomial interpretations)
- Apr 1 2019: Version 1.19 released (support WPO)
- Nov 26 2018: Version 1.18 released (fixed bug in encoding of ACKBO)
- Apr 30 2018: Version 1.17 released (support templates for LPO, KBO, polynomial and matrix interpretations; support external tool for dependency graph edge-estimation)
Download
The current version is 1.20. Get recent versions. Or directly access the mercurial repository for the latest development version.Contact
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.
Contributors
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- CaT (Complexity and Termination)
- ConCon (Conditional Confluence)
- KBCV (Knuth-Bendix Completion Visualizer)
- mkbTT (Multi Completion with Termination Tools)
- TcT (Tyrolean Complexity Tool)
- Wanda (A higher-order termination 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.15em\raisebox{-0.55ex}T\kern-0.15emT\kern-0.15em\raisebox{-0.55ex}2}%
}
The result should look approximately as follows 