Description
The Tyrolean Termination Tool 2 (TTT2) is a tool for automatically proving termination of rewrite systems. It is the completely redesigned successor of TTT. Current termination techniques include dependency pairs tranformation, approximated dependency graph, argument filtering, match-bounds, knuth-bendix order, lexicographic path order, matrix interpretation, polynomial interpretation, simple projection and subterm criterion, uncurrying and usable rules. A previous version of TTT2 took part at the international Termination Competition 2007 and 2008.In the following we concentrate on the part of TTT2 which implements the match-bound technique. For more general information, please check the official web site of TTT2.