Abstract
This paper describes the Tyrolean Termination Tool (\(\mathsf{T}\!_{\mbox{\sf T}}\!\mathsf{T}\) in the sequel), the successor of the Tsukuba Termination Tool [12]. We describe the differences between the two and explain the new features, some of which are not (yet) available in any other termination tool, in some detail. \(\mathsf{T}\!_{\mbox{\sf T}}\!\mathsf{T}\) is a tool for automatically proving termination of rewrite systems based on the dependency pair method of Arts and Giesl [3]. It produces high-quality output and has a convenient web interface. The tool is available at
http://cl2-informatik.uibk.ac.at/ttt
\(\mathsf{T}\!_{\mbox{\sf T}}\!\mathsf{T}\) incorporates several new improvements to the dependency pair method. In addition, it is now possible to run the tool in fully automatic mode on a collection of rewrite systems. Moreover, besides ordinary (first-order) rewrite systems, the tool accepts simply-typed applicative rewrite systems which are transformed into ordinary rewrite systems by the recent method of Aoto and Yamada [2].
In the next section we describe the differences between the semi automatic mode and the Tsukuba Termination Tool. Section 3 describes the fully automatic mode. In Section 4 we show a termination proof of a simply-typed applicative system obtained by \(\mathsf{T}\!_{\mbox{\sf T}}\!\mathsf{T}\). In Section 5 we describe how to input a collection of rewrite systems and how to interpret the resulting output. Some implementation details are given in Section 6. The final section contains a short comparison with other tools for automatically proving termination.
A preliminary description of the Tyrolean Termination Tool appeared in the proceedings of the 7th International Workshop on Termination, Technical Report AIB-2004-07, RWTH Aachen, pages 249–268, 2004.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Aoto, T., Yamada, T.: Termination of simply typed term rewriting by translation and labelling. In: Nieuwenhuis, R. (ed.) RTA 2003. LNCS, vol. 2706, pp. 380–394. Springer, Heidelberg (2003)
Aoto, T., Yamada, T.: Termination of simply-typed applicative term rewriting systems. In: Proc. 2nd HOR, Technical Report AIB-2004-03, RWTH Aachen, pp. 61–65 (2004)
Arts, T., Giesl, J.: Termination of term rewriting using dependency pairs. Theoretical Computer Science 236, 133–178 (2000)
Arts, T., Giesl, J.: A collection of examples for termination of term rewriting using dependency pairs. Technical Report AIB-2001-09, RWTH Aachen (2001)
Contejean, E., Marché, C., Monate, B., Urbain, X.: CiME version 2 (2000), Available at http://cime.lri.fr/
Contejean, E., Marché, C., Tomás, A.-P., Urbain, X.: Mechanically proving termination using polynomial interpretations. Research Report 1382, LRI (2004)
Dershowitz, N.: Termination by abstraction. In: Demoen, B., Lifschitz, V. (eds.) ICLP 2004. LNCS, vol. 3132, pp. 1–18. Springer, Heidelberg (2004)
Dick, J., Kalmus, J., Martin, U.: Automating the Knuth-Bendix ordering. Acta Infomatica 28, 95–119 (1990)
Fissore, O., Gnaedig, I., Kirchner, H.: CARIBOO: An induction based proof tool for termination with strategies. In: Proc. 4th PPDP, pp. 62–73. ACM Press, New York (2002)
Geser, A., Hofbauer, D., Waldmann, J.: Match-bounded string rewriting. Applicable Algebra in Engineering, Communication and Computing 15, 149–171 (2004)
Giesl, J., Thiemann, R., Schneider-Kamp, P., Falke, S.: Automated termination proofs with AProVE. In: van Oostrom, V. (ed.) RTA 2004. LNCS, vol. 3091, pp. 210–220. Springer, Heidelberg (2004)
Hirokawa, N., Middeldorp, A.: Tsukuba termination tool. In: Nieuwenhuis, R. (ed.) RTA 2003. LNCS, vol. 2706, pp. 311–320. Springer, Heidelberg (2003)
Hirokawa, N., Middeldorp, A.: Dependency pairs revisited. In: van Oostrom, V. (ed.) RTA 2004. LNCS, vol. 3091, pp. 249–268. Springer, Heidelberg (2004)
Hirokawa, N., Middeldorp, A.: Polynomial interpretations with negative coefficients. In: Buchberger, B., Campbell, J. (eds.) AISC 2004. LNCS (LNAI), vol. 3249, pp. 185–198. Springer, Heidelberg (2004)
Hirokawa, N., Middeldorp, A.: Automating the dependency pair method. In: Baader, F. (ed.) CADE 2003. LNCS (LNAI), vol. 2741, pp. 32–46. Springer, Heidelberg (2003)
Korovin, K., Voronkov, A.: Orienting rewrite rules with the Knuth-Bendix order. Information and Computation 183, 165–186 (2003)
Pierce, B.C.: Types and Programming Languages. MIT Press, Cambridge (2002)
Thiemann, R., Giesl, J.: Size-change termination for term rewriting. In: Nieuwenhuis, R. (ed.) RTA 2003. LNCS, vol. 2706, pp. 264–278. Springer, Heidelberg (2003)
Waldmann, J.: Matchbox: A tool for match-bounded string rewriting. In: van Oostrom, V. (ed.) RTA 2004. LNCS, vol. 3091, pp. 85–94. Springer, Heidelberg (2004)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2005 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Hirokawa, N., Middeldorp, A. (2005). Tyrolean Termination Tool. In: Giesl, J. (eds) Term Rewriting and Applications. RTA 2005. Lecture Notes in Computer Science, vol 3467. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-32033-3_14
Download citation
DOI: https://doi.org/10.1007/978-3-540-32033-3_14
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-25596-3
Online ISBN: 978-3-540-32033-3
eBook Packages: Computer ScienceComputer Science (R0)