Skip to main content
SpringerLink
Log in

Match-Bounds with Dependency Pairs for Proving Termination of Rewrite Systems

  • Conference paper
Language and Automata Theory and Applications (LATA 2008)

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

Abstract

The match-bound technique is a recent and elegant method to prove the termination of rewrite systems using automata techniques. To increase the applicability of the method we incorporate it into the dependency pair framework. The key to this is the introduction of two new enrichments which take the special properties of dependency pair problems into account.

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

Access this chapter

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

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Arts, T., Giesl, J.: Termination of term rewriting using dependency pairs. TCS 236, 133–178 (2000)

    Article  MATH  MathSciNet  Google Scholar 

  2. Baader, F., Nipkow, T.: Term Rewriting and All That. Cambridge University Press, Cambridge (1998)

    Google Scholar 

  3. Comon, H., Dauchet, M., Gilleron, R., Jacquemard, F., Lugiez, D., Tison, S., Tommasi, M.: Tree automata techniques and applications (2002), www.grappa.univ-lille3.fr/tata

  4. Dershowitz, N.: Termination of linear rewriting systems (preliminary version). In: Even, S., Kariv, O. (eds.) ICALP 1981. LNCS, vol. 115, pp. 448–458. Springer, Heidelberg (1981)

    Google Scholar 

  5. Geser, A., Hofbauer, D., Waldmann, J.: Match-bounded string rewriting systems. AAECC 15(3-4), 149–171 (2004)

    Article  MATH  MathSciNet  Google Scholar 

  6. Geser, A., Hofbauer, D., Waldmann, J.: Termination proofs for string rewriting systems via inverse match-bounds. JAR 34(4), 365–385 (2005)

    Article  MATH  MathSciNet  Google Scholar 

  7. Geser, A., Hofbauer, D., Waldmann, J., Zantema, H.: Finding finite automata that certify termination of string rewriting systems. International Journal of Foundations of Computer Science 16(3), 471–486 (2005)

    Article  MATH  MathSciNet  Google Scholar 

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

    MATH  MathSciNet  Google Scholar 

  9. Geupel, O.: Overlap closures and termination of term rewriting systems. Report MIP-8922, Universität Passau (1989)

    Google Scholar 

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

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

    Google Scholar 

  12. Giesl, J., Thiemann, R., Schneider-Kamp, P.: Proving and disproving termination of higher-order functions. In: Gramlich, B. (ed.) FroCos 2005. LNCS (LNAI), vol. 3717, pp. 216–231. Springer, Heidelberg (2005)

    Chapter  Google Scholar 

  13. Giesl, J., Thiemann, R., Schneider-Kamp, P., Falke, S.: Mechanizing and improving dependency pairs. JAR 37(3), 155–203 (2006)

    Article  MATH  MathSciNet  Google Scholar 

  14. Hirokawa, N., Middeldorp, A.: Automating the dependency pair method. I&C 199(1,2), 172–199 (2005)

    MATH  MathSciNet  Google Scholar 

  15. Hirokawa, N., Middeldorp, A.: Tyrolean termination tool: Techniques and features. I&C 205(4), 474–511 (2007)

    MATH  MathSciNet  Google Scholar 

  16. Jambox, http://joerg.endrullis.de/

  17. Korp, M., Middeldorp, A.: Proving termination of rewrite systems using bounds. In: Baader, F. (ed.) RTA 2007. LNCS, vol. 4533, pp. 273–287. Springer, Heidelberg (2007)

    Chapter  Google Scholar 

  18. Middeldorp, A.: Approximating dependency graphs using tree automata techniques. In: Goré, R.P., Leitsch, A., Nipkow, T. (eds.) IJCAR 2001. LNCS (LNAI), vol. 2083, pp. 593–610. Springer, Heidelberg (2001)

    Chapter  Google Scholar 

  19. Nagaya, T., Toyama, Y.: Decidability for left-linear growing term rewriting systems. I&C 178(2), 499–514 (2002)

    MATH  MathSciNet  Google Scholar 

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

  21. Tyrolean Termination Tool 2, http://colo6-c703.uibk.ac.at/ttt2

  22. Waldmann, J.: Matchbox: A tool for match-bounded string rewriting. In: van Oostrom, V. (ed.) RTA 2004. LNCS, vol. 3091, pp. 85–94. Springer, Heidelberg (2004)

    Google Scholar 

  23. Zantema, H.: Termination of rewriting proved automatically. JAR 34(2), 105–139 (2005)

    Article  MATH  MathSciNet  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Institute of Computer Science, University of Innsbruck, Austria

    Martin Korp & Aart Middeldorp

Authors
  1. Martin Korp
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Aart Middeldorp
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Research Group on Mathematical Linguistics, Rovira i Virgili University, Plaza Imperial Tàrraco 1, 43005, Tarragona, Spain

    Carlos Martín-Vide

  2. Fachbereich Elektrotechnik/Informatik, Universität Kassel, Wilhelmshöher Allee 73, 34121, Kassel, Germany

    Friedrich Otto

  3. Fachbereich 4, Abteilung Informatik/Wirtschaftsinformatik, Universität Trier, Campus II, Gebäude H, 54286, Trier, Germany

    Henning Fernau

Rights and permissions

Reprints and permissions

Copyright information

© 2008 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Korp, M., Middeldorp, A. (2008). Match-Bounds with Dependency Pairs for Proving Termination of Rewrite Systems. In: Martín-Vide, C., Otto, F., Fernau, H. (eds) Language and Automata Theory and Applications. LATA 2008. Lecture Notes in Computer Science, vol 5196. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-88282-4_30

Download citation

  • DOI: https://doi.org/10.1007/978-3-540-88282-4_30

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-88281-7

  • Online ISBN: 978-3-540-88282-4

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation