Abstract
We present a tool for automatically proving termination of first-order rewrite systems. The tool is based on the dependency pair method of Arts and Giesl. It incorporates several new ideas that make the method more efficient. The tool produces high-quality output and has a convenient web interface.
Partially supported by the Grant-in-Aid for Scientific Research (C)(2) 13224006 of the Ministry of Education, Culture, Sports, Science and Technology of Japan.
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.
Similar content being viewed by others
References
T. Arts. System description: The dependency pair method. In Proc. 11th RTA, volume 1833 of LNCS, pages 261–264, 2001.
T. Arts and J. Giesl. Termination of term rewriting using dependency pairs. Theoretical Computer Science, 236:133–178, 2000.
T. Arts and J. Giesl. A collection of examples for termination of term rewriting using dependency pairs. Technical Report AIB-2001-09, RWTH Aachen, 2001. Available at http://aib.informatik.rwth-aachen.de/.
C. Borralleras, M. Ferreira, and A. Rubio. Complete monotonic semantic path orderings. In Proc. 17th CADE, volume 1831 of LNAI, pages 346–364, 2000.
E. Contejean, C. Marché, B. Monate, and X. Urbain. CiME version 2, 2000. Available at http://cime.lri.fr/.
N. Dershowitz. 33 Examples of termination. In French Spring School of Theoretical Computer Science, volume 909 of LNCS, pages 16–26, 1995.
J. Giesl, T. Arts, and E. Ohlebusch. Modular termination proofs for rewriting using dependency pairs. Journal of Symbolic Computation, 34(1):21–58, 2002.
N. Hirokawa and A. Middeldorp. Automating the dependency pair method. In Proc. 19th CADE, LNAI, 2003. To appear.
D.J. King and J. Launchbury. Structuring depth-first search algorithms in Haskell. In Proc. 22nd POPL, pages 344–354, 1995.
K. Korovin and A. Voronkov. Verifying orientability of rewrite rules using the Knuth-Bendix order. In Proc. 12th RTA, volume 2051 of LNCS, pages 137–153, 2001.
A. Middeldorp. Approximations for strategies and termination. In Proc. 2nd WRS, volume 70(6) of Electronic Notes in Theoretical Computer Science, 2002.
E. Ohlebusch. Hierarchical termination revisited. Information Processing Letters, 84(4):207–214, 2002.
J. Steinbach. Automatic termination proofs with transformation orderings. In Proc. 6th RTA, volume 914 of LNCS, pages 11–25, 1995.
J. Steinbach and U. Kühler. Check your ordering — termination proofs and open problems. Technical Report SR-90-25, Universität Kaiserslautern, 1990.
Joachim Steinbach. Simplification orderings: History of results. Fundamenta Informaticae, 24:47–87, 1995.
X. Urbain. Automated incremental termination proofs for hierarchically defined term rewriting systems. In Proc. IJCAR, volume 2083 of LNAI, pages 485–498, 2001.
X. Urbain. Modular & incremental automated termination proofs. Journal of Automated Reasoning, 2003. To appear.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2003 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Hirokawa, N., Middeldorp, A. (2003). Tsukuba Termination Tool. In: Nieuwenhuis, R. (eds) Rewriting Techniques and Applications. RTA 2003. Lecture Notes in Computer Science, vol 2706. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-44881-0_22
Download citation
DOI: https://doi.org/10.1007/3-540-44881-0_22
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-40254-1
Online ISBN: 978-3-540-44881-5
eBook Packages: Springer Book Archive