Tyrolean termination tool: Techniques and features

The Tyrolean Termination Tool (TTT for short) is a powerful tool for automatically proving termination of rewrite systems. It incorporates several new refinements of the dependency pair method that are easy to implement, increase the power of the method, result in simpler termination proofs, and make the method more efficient. TTT employs polynomial interpretations with negative coefficients, like x − 1 for a unary function symbol or x − y for a binary function symbol, which are useful for extending the class of rewrite systems that can be proved terminating automatically. Besides a detailed account of these techniques, we describe the convenient web interface of TTT and provide some implementation details.