Skip to main content
SpringerLink
Log in
Book cover

International Conference on Rewriting Techniques and Applications

RTA 2006: Term Rewriting and Applications pp 257–266Cite as

TPA: Termination Proved Automatically

  • Conference paper

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 4098))

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.

Chapter
USD   29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD   39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD   54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Learn about institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. The termination competition, http://www.lri.fr/~marche/termination-competition

  2. 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)

    Chapter  Google Scholar 

  3. Arts, T., Giesl, J.: Termination of term rewriting using dependency pairs. Theor. Comput. Sci. 236(1–2), 133–178 (2000)

    Article  MATH  MathSciNet  Google Scholar 

  4. Cherifa, A.B., Lescanne, P.: Termination of rewriting systems by polynomial interpretations and its implementation. Sci. Comput. Program 9(2), 137–159 (1987)

    Article  MATH  Google Scholar 

  5. Contejean, E., Marché, C., Monate, B., Urbain, X.: Proving termination of rewriting with c i me, pp. 71–73 (2003), http://cime.lri.fr

  6. Dershowitz, N.: Orderings for term-rewriting systems. Theor. Comput. Sci. 17, 279–301 (1982)

    Article  MATH  MathSciNet  Google Scholar 

  7. 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)

    Google Scholar 

  8. 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)

    Chapter  Google Scholar 

  9. Giesl, J., Zantema, H.: Liveness in rewriting. In: Nieuwenhuis, R. (ed.) RTA 2003. LNCS, vol. 2706, pp. 321–336. Springer, Heidelberg (2003)

    Chapter  Google Scholar 

  10. Hardin, T., Laville, A.: Proof of termination of the rewriting system SUBST on CCL. Theor. Comput. Sci. 46(2-3), 305–312 (1986)

    Article  MATH  MathSciNet  Google Scholar 

  11. Hirokawa, N., Middeldorp, A.: Tyrolean termination tool. In: Giesl, J. (ed.) RTA 2005. LNCS, vol. 3467, pp. 175–184. Springer, Heidelberg (2005)

    Chapter  Google Scholar 

  12. 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)

    Chapter  Google Scholar 

  13. 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)

    Chapter  Google Scholar 

  14. Lankford, D.S.: On proving term rewriting systems are noetherian. Tech. Rep. MTP-3, Louisiana Tech. Univ., Ruston (1979)

    Google Scholar 

  15. 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)

    Chapter  Google Scholar 

  16. Zantema, H.: Termination of term rewriting by semantic labelling. Fundam. Inform. 24(1/2), 89–105 (1995)

    MATH  MathSciNet  Google Scholar 

  17. Zantema, H.: Torpa: Termination of rewriting proved automatically. In: van Oostrom, V. (ed.) RTA 2004. LNCS, vol. 3091, pp. 95–104. Springer, Heidelberg (2004)

    Chapter  Google Scholar 

  18. 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)

    Chapter  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Technical University of Eindhoven, P.O. Box 513, 5600 MB, Eindhoven, The Netherlands

    Adam Koprowski

Authors
  1. Adam Koprowski
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Carnegie Mellon University,  

    Frank Pfenning

Rights and permissions

Reprints 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)

Publish with us

Policies and ethics

Search

Navigation