[go: up one dir, main page]
More Web Proxy on the site http://driver.im/
Skip to main content

Tyrolean Termination Tool 2

  • Conference paper
Rewriting Techniques and Applications (RTA 2009)

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

Included in the following conference series:

Abstract

This paper describes the second edition of the Tyrolean Termination Tool—a fully automatic termination analyzer for first-order term rewrite systems. The main features of this tool are its (non-)termination proving power, its speed, its flexibility due to a strategy language, and the fact that the source code of the whole project is freely available. The clean design together with a stand-alone OCaml library for term rewriting, make it a perfect starting point for other tools concerned with rewriting as well as experimental implementations of new termination methods.

This research is supported by FWF (Austrian Science Fund) project P18763.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Subscribe and save

Springer+ Basic
£29.99 /Month
  • Get 10 units per month
  • Download Article/Chapter or eBook
  • 1 Unit = 1 Article or 1 Chapter
  • Cancel anytime
Subscribe now

Buy Now

Chapter
GBP 19.95
Price includes VAT (United Kingdom)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
GBP 35.99
Price includes VAT (United Kingdom)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
GBP 44.99
Price includes VAT (United Kingdom)
  • 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

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

Similar content being viewed by others

References

  1. Dutertre, B., de Moura, L.: A fast linear-arithmetic solver for DPLL(T). In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol. 4144, pp. 81–94. Springer, Heidelberg (2006)

    Chapter  Google Scholar 

  2. Eén, N., Sörensson, N.: An extensible SAT-solver. In: Giunchiglia, E., Tacchella, A. (eds.) SAT 2003. LNCS, vol. 2919, pp. 502–518. Springer, Heidelberg (2004)

    Chapter  Google Scholar 

  3. Endrullis, J., Waldmann, J., Zantema, H.: Matrix interpretations for proving termination of rewrite systems. Journal of Automated Reasoning 40(2-3), 195–220 (2008)

    Article  MathSciNet  MATH  Google Scholar 

  4. Fuhs, C., Giesl, J., Middeldorp, A., Schneider-Kamp, P., Thiemann, R., Zankl, H.: Maximal termination. In: Voronkov, A. (ed.) RTA 2008. LNCS, vol. 5117, pp. 110–125. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

  5. Geser, A., Hofbauer, D., Waldmann, J., Zantema, H.: On tree automata that certify termination of left-linear term rewriting systems. Information and Computation 205(4), 512–534 (2007)

    Article  MathSciNet  MATH  Google Scholar 

  6. Giesl, J., Schneider-Kamp, P., Thiemann, R.: AProVE 1.2: Automatic termination proofs in the dependency pair framework. In: Furbach, U., Shankar, N. (eds.) IJCAR 2006. LNCS (LNAI), vol. 4130, pp. 281–286. Springer, Heidelberg (2006)

    Chapter  Google Scholar 

  7. Giesl, J., Thiemann, R., Schneider-Kamp, P.: The dependency pair framework: Combining techniques for automated termination proofs. In: Baader, F., Voronkov, A. (eds.) LPAR 2004. LNCS (LNAI), vol. 3452, pp. 301–331. Springer, Heidelberg (2005)

    Chapter  Google Scholar 

  8. Giesl, J., Thiemann, R., Schneider-Kamp, P., Falke, S.: Mechanizing and improving dependency pairs. Journal of Automated Reasoning 37(3), 155–203 (2006)

    Article  MathSciNet  MATH  Google Scholar 

  9. Hirokawa, N., Middeldorp, A.: Uncurrying for termination. In: Kesner, D., van Raamsdonk, F., Stehr, M.O. (eds.) HOR 2006, pp. 19–24 (2006)

    Google Scholar 

  10. Hirokawa, N., Middeldorp, A.: Tyrolean Termination Tool: Techniques and features. Information and Computation 205(4), 474–511 (2007)

    Article  MathSciNet  MATH  Google Scholar 

  11. Hirokawa, N., Middeldorp, A., Zankl, H.: Uncurrying for termination. In: Cervesato, I., Veith, H., Voronkov, A. (eds.) LPAR 2008. LNCS (LNAI), vol. 5330, pp. 667–681. Springer, Heidelberg (2008)

    Google Scholar 

  12. Hofbauer, D., Waldmann, J.: Termination of string rewriting with matrix interpretations. In: Pfenning, F. (ed.) RTA 2006. LNCS, vol. 4098, pp. 328–342. Springer, Heidelberg (2006)

    Chapter  Google Scholar 

  13. Koprowski, A., Waldmann, J.: Arctic termination ... below zero. In: Voronkov, A. (ed.) RTA 2008. LNCS, vol. 5117, pp. 202–216. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

  14. Korp, M., Middeldorp, A.: Match-bounds revisited. Information and Computation (2009), doi:10.1016/j.ic.2009.02.010

    Google Scholar 

  15. Moser, G., Schnabl, A., Waldmann, J.: Complexity analysis of term rewriting based on matrix and context dependent interpretations. In: Hariharan, R., Mukund, M., Vinay, V. (eds.) FSTTCS 2008. DROPS, vol. 1762, pp. 304–315. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, Dagstuhl (2008)

    Google Scholar 

  16. Moser, G., Schnabl, A.: Proving quadratic derivational complexities using context dependent interpretations. In: Voronkov, A. (ed.) RTA 2008. LNCS, vol. 5117, pp. 276–290. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

  17. Nipkow, T., Paulson, L.C., Wenzel, M.T.: Isabelle/HOL. LNCS, vol. 2283. Springer, Heidelberg (2002)

    MATH  Google Scholar 

  18. Payet, É.: Loop detection in term rewriting using the eliminating unfoldings. Theoretical Computer Science 403(2-3), 307–327 (2008)

    Article  MathSciNet  MATH  Google Scholar 

  19. Plaisted, D.A., Greenbaum, S.: A structure-preserving clause form translation. Journal of Symbolic Computation 2(3), 293–304 (1986)

    Article  MathSciNet  MATH  Google Scholar 

  20. Sato, H., Winkler, S., Kurihara, M., Middeldorp, A.: Multi-completion with termination tools (system description). In: Armando, A., Baumgartner, P., Dowek, G. (eds.) IJCAR 2008. LNCS (LNAI), vol. 5195, pp. 306–312. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

  21. Sternagel, C., Middeldorp, A.: Root-labeling. In: Voronkov, A. (ed.) RTA 2008. LNCS, vol. 5117, pp. 336–350. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

  22. Thiemann, R.: The DP Framework for Proving Termination of Term Rewriting. PhD thesis, RWTH Aachen, Available as technical report AIB-2007-17 (2007)

    Google Scholar 

  23. Thiemann, R., Sternagel, C.: Loops under strategies. In: Treinen, R. (ed.) RTA 2009. LNCS, vol. 5595, pp. 17–31. Springer, Heidelberg (2009)

    Google Scholar 

  24. Zankl, H., Hirokawa, N., Middeldorp, A.: KBO orientability. Journal of Automated Reasoning (2009), doi:10.1007/s10817-009-9131-z

    Google Scholar 

  25. Zankl, H., Middeldorp, A.: Nontermination of string rewriting using SAT. In: Hofbauer, D., Serebrenik, A. (eds.) WST 2007, pp. 56–59 (2007)

    Google Scholar 

  26. Zankl, H., Middeldorp, A.: Increasing interpretations. Annals of Mathematics and Artificial Intelligence (to appear, 2009)

    Google Scholar 

Download references

Author information

Authors and Affiliations

Authors

Editor information

Editors and Affiliations

Rights and permissions

Reprints and permissions

Copyright information

© 2009 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Korp, M., Sternagel, C., Zankl, H., Middeldorp, A. (2009). Tyrolean Termination Tool 2. In: Treinen, R. (eds) Rewriting Techniques and Applications. RTA 2009. Lecture Notes in Computer Science, vol 5595. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-02348-4_21

Download citation

  • DOI: https://doi.org/10.1007/978-3-642-02348-4_21

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-642-02347-7

  • Online ISBN: 978-3-642-02348-4

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics