-
Notifications
You must be signed in to change notification settings - Fork 0
TTT2
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.
TTT2 accepts the input format for Term Rewrite Systems as specified in TPDB (XML and old TRS format). Moreover, also several variations for relative termination or strategy annotations (innermost rewriting,...) are accepted.
termination and non-termination
Dependency Pair framework, various interpretation methods, transformation methods, ...
(for a complete list call the executable with ./ttt2 --processors)
- SAT solvers: MiniSat, MiniSat+, PicoSAT
- SMT solvers: MiniSMT (which is part of TTT2), in some cases Z3 (others can be used via flags if installed on user system)
- nonreachability analysis: nonreach can be used in the strategy to improve edge estimation
- website: http://cl-informatik.uibk.ac.at/software/ttt2/
- repository: http://cl2-informatik.uibk.ac.at/mercurial.cgi/ttt2/
- web interface: http://colo6-c703.uibk.ac.at/ttt2/web/
The termination community maintains a database with thousands of examples, called Termination Problem DataBase (TPDB).
For some methods (LPO, KBO, polynomial interpretations, matrix interpretations, weighted path order) TTT2 can check specific handwritten
proofs and verify them afterwards with CeTA. Furthermore, via a config file one
can specify complex strategies for TTT2 (see ./ttt2 --help for more information). In case of bugs please contact the mailing list
ttt2 at informatik dot uibk dot ac dot at.
- Martin Korp, Christian Sternagel, Harald Zankl, and Aart Middeldorp
Tyrolean Termination Tool 2
In Proceedings of the 20th International Conference on Rewriting Techniques and Applications (RTA 2009), LNCS 5595, pp. 295 – 304, 2009. DOI