Abstract
TPA is a tool for proving termination of term rewrite systems (TRSs) in a fully automated fashion. The distinctive feature of TPA is the support for relative termination and the use of the technique of semantic labelling with natural numbers. Thanks to the latter, TPA is capable of delivering automated termination proofs for some difficult TRSs for which all other tools fail.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsPreview
Unable to display preview. Download preview PDF.
References
The termination competition, http://www.lri.fr/~marche/termination-competition
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)
Arts, T., Giesl, J.: Termination of term rewriting using dependency pairs. Theor. Comput. Sci. 236(1–2), 133–178 (2000)
Cherifa, A.B., Lescanne, P.: Termination of rewriting systems by polynomial interpretations and its implementation. Sci. Comput. Program 9(2), 137–159 (1987)
Contejean, E., Marché, C., Monate, B., Urbain, X.: Proving termination of rewriting with c i me, pp. 71–73 (2003), http://cime.lri.fr
Dershowitz, N.: Orderings for term-rewriting systems. Theor. Comput. Sci. 17, 279–301 (1982)
Ferreira, M.C.F., Zantema, H.: Dummy elimination: Making termination easier. In: Reichel, H. (ed.) FCT 1995. LNCS, vol. 965, pp. 243–252. Springer, Heidelberg (1995)
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)
Giesl, J., Zantema, H.: Liveness in rewriting. In: Nieuwenhuis, R. (ed.) RTA 2003. LNCS, vol. 2706, pp. 321–336. Springer, Heidelberg (2003)
Hardin, T., Laville, A.: Proof of termination of the rewriting system SUBST on CCL. Theor. Comput. Sci. 46(2-3), 305–312 (1986)
Hirokawa, N., Middeldorp, A.: Tyrolean termination tool. In: Giesl, J. (ed.) RTA 2005. LNCS, vol. 3467, pp. 175–184. Springer, Heidelberg (2005)
Koprowski, A., Zantema, H.: Proving liveness with fairness using rewriting. In: Gramlich, B. (ed.) FroCos 2005. LNCS (LNAI), vol. 3717, pp. 232–247. Springer, Heidelberg (2005)
Koprowski, A., Zantema, H.: Automation of Recursive Path Ordering for Infinite Labelled Rewrite Systems. In: Furbach, U., Shankar, N. (eds.) IJCAR 2006. LNCS (LNAI), vol. 4130, pp. 332–346. Springer, Heidelberg (2006)
Lankford, D.S.: On proving term rewriting systems are noetherian. Tech. Rep. MTP-3, Louisiana Tech. Univ., Ruston (1979)
Lucas, S., Meseguer, J.: Termination of fair computations in term rewriting. In: Sutcliffe, G., Voronkov, A. (eds.) LPAR 2005. LNCS (LNAI), vol. 3835, pp. 184–198. Springer, Heidelberg (2005)
Zantema, H.: Termination of term rewriting by semantic labelling. Fundam. Inform. 24(1/2), 89–105 (1995)
Zantema, H.: Torpa: Termination of rewriting proved automatically. In: van Oostrom, V. (ed.) RTA 2004. LNCS, vol. 3091, pp. 95–104. Springer, Heidelberg (2004)
Zantema, H.: Reducing Right-Hand Sides for Termination. In: Middeldorp, A., van Oostrom, V., van Raamsdonk, F., de Vrijer, R. (eds.) Processes, Terms and Cycles: Steps on the Road to Infinity. LNCS, vol. 3838, pp. 173–197. Springer, Heidelberg (2005)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2006 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Koprowski, A. (2006). TPA: Termination Proved Automatically. In: Pfenning, F. (eds) Term Rewriting and Applications. RTA 2006. Lecture Notes in Computer Science, vol 4098. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11805618_19
Download citation
DOI: https://doi.org/10.1007/11805618_19
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-36834-2
Online ISBN: 978-3-540-36835-9
eBook Packages: Computer ScienceComputer Science (R0)