Abstract
The tool TORPA (Termination of Rewriting Proved Automatically) can be used to prove termination of string rewriting systems (SRSs) fully automatically. The underlying techniques include semantic labelling, polynomial interpretations, recursive path order, the dependency pair method and match bounds of right hand sides of forward closures.
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Arts, T., Giesl, J.: Termination of term rewriting using dependency pairs. Theoretical Computer Science 236, 133–178 (2000)
Ben-Cherifa, A., Lescanne, P.: Termination of rewriting systems by polynomial interpretations and its implementation. Science of Computer Programming 9, 137–159 (1987)
Boralleras, C., Rubio, A.: Termptation: termination proof techniques automation, Available at http://www.lsi.upc.es/~albert/
Contejean, E., Marché, C., Monate, B., Urbain, X.: The CiME rewrite tool, Available at http://cime.lri.fr/
Dershowitz, N.: Orderings for term-rewriting systems. Theoretical Computer Science 17, 279–301 (1982)
Giesl, J., et al.: Automated program verification environment (AProVE), Available at http://www-i2.informatik.rwth-aachen.de/AProVE/
Geser, A., Hofbauer, D., Waldmann, J.: Match-bounded string rewriting. Technical Report 2003-09, National Institute of Aerospace, Hampton, VA (2003) (submitted for publication in a journal)
Giesl, J., Zantema, H.: Liveness in rewriting. In: Nieuwenhuis, R. (ed.) RTA 2003. LNCS, vol. 2706, pp. 321–336. Springer, Heidelberg (2003)
Hirokawa, N., Middeldorp, A.: Tsukuba termination tool. In: Nieuwenhuis, R. (ed.) RTA 2003. LNCS, vol. 2706, pp. 311–320. Springer, Heidelberg (2003)
Lankford, D.S.: On proving term rewriting systems are noetherian. Technical report MTP 3, Louisiana Technical University (1979)
Zantema, H.: Termination of term rewriting: Interpretation and type elimination. Journal of Symbolic Computation 17, 23–50 (1994)
Zantema, H.: Termination of term rewriting by semantic labelling. Fundamenta Informaticae 24, 89–105 (1995)
Zantema, H.: Termination. In: Term Rewriting Systems, by Terese, pp. 181–259. Cambridge University Press, Cambridge (2003)
Zantema, H.: Termination of string rewriting proved automatically. Technical Report CS-report 03-14, Eindhoven University of Technology, Submitted, available via (2003), http://www.win.tue.nl/inf/onderzoek/en_index.html
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2004 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Zantema, H. (2004). TORPA: Termination of Rewriting Proved Automatically. In: van Oostrom, V. (eds) Rewriting Techniques and Applications. RTA 2004. Lecture Notes in Computer Science, vol 3091. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-25979-4_7
Download citation
DOI: https://doi.org/10.1007/978-3-540-25979-4_7
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-22153-1
Online ISBN: 978-3-540-25979-4
eBook Packages: Springer Book Archive