Tyrolean termination tool: Techniques and features

The Tyrolean Termination Tool (T T T 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. T T T 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 T T T and provide some implementation details.

Authors

• Nao Hirokawa
• Aart Middeldorp

Keywords

• Term rewriting
• Termination
• Automation
• Dependency pair method
• Polynomial interpretations