Tyrolean termination tool: Techniques and features

9 years 2 months ago
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. Key words: Term rewriting, Termination, Automation, Dependency pair method, Polynomial interpretations
Nao Hirokawa, Aart Middeldorp
Added 14 Dec 2010
Updated 14 Dec 2010
Type Journal
Year 2007
Authors Nao Hirokawa, Aart Middeldorp
Comments (0)