Skip to main content
SpringerLink
Log in

Termination Analysis by Dependency Pairs and Inductive Theorem Proving

  • Conference paper
Automated Deduction – CADE-22 (CADE 2009)

Part of the book series: Lecture Notes in Computer Science ((LNAI,volume 5663))

Included in the following conference series:

Abstract

Current techniques and tools for automated termination analysis of term rewrite systems (TRSs) are already very powerful. However, they fail for algorithms whose termination is essentially due to an inductive argument. Therefore, we show how to couple the dependency pair method for TRS termination with inductive theorem proving. As confirmed by the implementation of our new approach in the tool AProVE, now TRS termination techniques are also successful on this important class of algorithms.

Supported by the DFG Research Training Group 1298 (AlgoSyn), the DFG grant GI 274/5-2, and the G.I.F. grant 966-116.6.

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. AProVE website, http://aprove.informatik.rwth-aachen.de/eval/Induction/

  2. Arts, T., Giesl, J.: Termination of term rewriting using dependency pairs. Theoretical Computer Science 236, 133–178 (2000)

    Article  MathSciNet  MATH  Google Scholar 

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

    Google Scholar 

  4. Bouhoula, A., Rusinowitch, M.: SPIKE: A system for automatic inductive proofs. In: Alagar, V.S., Nivat, M. (eds.) AMAST 1995. LNCS, vol. 936, pp. 576–577. Springer, Heidelberg (1995)

    Chapter  Google Scholar 

  5. Boyer, R.S., Moore, J.S.: A Computational Logic. Academic Press, London (1979)

    MATH  Google Scholar 

  6. Brauburger, J., Giesl, J.: Termination analysis by inductive evaluation. In: Kirchner, C., Kirchner, H. (eds.) CADE 1998. LNCS (LNAI), vol. 1421, pp. 254–269. Springer, Heidelberg (1998)

    Chapter  Google Scholar 

  7. Bundy, A.: The automation of proof by mathematical induction. In: Robinson, J.A., Voronkov, A. (eds.) Handbook of Automated Reasoning, vol. 1, pp. 845–911. Elsevier & MIT (2001)

    Google Scholar 

  8. Comon, H.: Inductionless induction. In: Robinson, J.A., Voronkov, A. (eds.) Handbook of Automated Reasoning, vol. 1, pp. 913–962. Elsevier & MIT (2001)

    Google Scholar 

  9. Fuhs, C., Giesl, J., Middeldorp, A., Schneider-Kamp, P., Thiemann, R., Zankl, H.: SAT solving for termination analysis with polynomial interpretations. In: Marques-Silva, J., Sakallah, K.A. (eds.) SAT 2007. LNCS, vol. 4501, pp. 340–354. Springer, Heidelberg (2007)

    Chapter  Google Scholar 

  10. Giesl, J.: Termination analysis for functional programs using term orderings. In: Mycroft, A. (ed.) SAS 1995. LNCS, vol. 983, pp. 154–171. Springer, Heidelberg (1995)

    Chapter  Google Scholar 

  11. Giesl, J., Thiemann, R., Schneider-Kamp, P.: The DP 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 

  12. Giesl, J., Swiderski, S., Schneider-Kamp, P., Thiemann, R.: Automated termination analysis for Haskell: From term rewriting to programming languages. In: Pfenning, F. (ed.) RTA 2006. LNCS, vol. 4098, pp. 297–312. Springer, Heidelberg (2006)

    Chapter  Google Scholar 

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

    Chapter  Google Scholar 

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

  15. Giesl, J., Thiemann, R., Swiderski, S., Schneider-Kamp, P.: Proving termination by bounded increase. In: Pfenning, F. (ed.) CADE 2007. LNCS (LNAI), vol. 4603, pp. 443–459. Springer, Heidelberg (2007)

    Chapter  Google Scholar 

  16. Gnaedig, I., Kirchner, H.: Termination of rewriting under strategies. ACM Transactions on Computational Logic 10(3) (2008)

    Google Scholar 

  17. Gramlich, B.: Abstract relations between restricted termination and confluence properties of rewrite systems. Fundamenta Informaticae 24(1-2), 2–23 (1995)

    MathSciNet  MATH  Google Scholar 

  18. Hirokawa, N., Middeldorp, A.: Automating the dependency pair method. Information and Computation 199(1-2), 172–199 (2005)

    Article  MathSciNet  MATH  Google Scholar 

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

    Article  MathSciNet  MATH  Google Scholar 

  20. Kapur, D., Musser, D.R.: Proof by consistency. Artif. Int. 31(2), 125–157 (1987)

    Article  MathSciNet  MATH  Google Scholar 

  21. Kaufmann, M., Manolios, P., Moore, J.S.: Computer-Aided Reasoning: An Approach. Kluwer, Dordrecht (2000)

    Google Scholar 

  22. Krauss, A.: Certified size-change termination. In: Pfenning, F. (ed.) CADE 2007. LNCS (LNAI), vol. 4603, pp. 460–475. Springer, Heidelberg (2007)

    Chapter  Google Scholar 

  23. Lankford, D.: On proving term rewriting systems are Noetherian. Technical Report MTP-3, Louisiana Technical University, Ruston, LA, USA (1979)

    Google Scholar 

  24. Lucas, S., Meseguer, J.: Order-sorted dependency pairs. In: Proc. PPDP 2008, pp. 108–119. ACM Press, New York (2008)

    Google Scholar 

  25. Manolios, P., Vroon, D.: Termination analysis with calling context graphs. In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol. 4144, pp. 401–414. Springer, Heidelberg (2006)

    Chapter  Google Scholar 

  26. Middeldorp, A., Zantema, H.: Personal communication (2008)

    Google Scholar 

  27. Ohlebusch, E.: Termination of logic programs: Transformational approaches revisited. Appl. Algebra in Engineering, Comm. and Computing 12, 73–116 (2001)

    Article  MathSciNet  MATH  Google Scholar 

  28. Panitz, S.E., Schmidt-Schauß, M.: TEA: Automatically proving termination of programs in a non-strict higher-order functional language. In: Van Hentenryck, P. (ed.) SAS 1997. LNCS, vol. 1302, pp. 345–360. Springer, Heidelberg (1997)

    Chapter  Google Scholar 

  29. Plaisted, D.A.: Equational reasoning and term rewriting systems. In: Gabbay, D.M., Hogger, C.J., Robinson, J.A. (eds.) Handbook of Logic in Artificial Intelligence and Logic Programming, Oxford, vol. 1, pp. 273–364 (1993)

    Google Scholar 

  30. van de Pol, J.: Modularity in many-sorted term rewriting. Master’s Thesis, Utrecht University (1992), http://homepages.cwi.nl/~vdpol/papers/

  31. Schneider-Kamp, P., Giesl, J., Serebrenik, A., Thiemann, R.: Automated termination proofs for logic programs by term rewriting. ACM Transactions on Computational Logic (to appear, 2009)

    Google Scholar 

  32. Walther, C.: On proving the termination of algorithms by machine. Artificial Intelligence 71(1), 101–157 (1994)

    Article  MathSciNet  MATH  Google Scholar 

  33. Walther, C.: Mathematical induction. In: Gabbay, D., Hogger, C.J., Robinson, J.A. (eds.) Handbook of Logic in AI and Logic Programming, Oxford, vol. 2, pp. 127–228 (1994)

    Google Scholar 

  34. Walther, C., Schweitzer, S.: About VeriFun. In: Baader, F. (ed.) CADE 2003. LNCS (LNAI), vol. 2741, pp. 322–327. Springer, Heidelberg (2003)

    Chapter  Google Scholar 

  35. Zantema, H.: Termination of term rewriting: Interpretation and type elimination. Journal of Symbolic Computation 17(1), 23–50 (1994)

    Article  MathSciNet  MATH  Google Scholar 

  36. Zhang, H., Kapur, D., Krishnamoorthy, M.S.: A mechanizable induction principle for equational specifications. In: Lusk, E., Overbeek, R. (eds.) CADE 1988. LNCS (LNAI), vol. 310, pp. 162–181. Springer, Heidelberg (1988)

    Chapter  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. LuFG Informatik 2, RWTH Aachen University, Germany

    Stephan Swiderski, Michael Parting, Jürgen Giesl & Carsten Fuhs

  2. Dept. of Mathematics & CS, University of Southern Denmark, Odense, Denmark

    Peter Schneider-Kamp

Authors
  1. Stephan Swiderski
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Michael Parting
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Jürgen Giesl
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Carsten Fuhs
    View author publications

    You can also search for this author in PubMed Google Scholar

  5. Peter Schneider-Kamp
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. School of Computer Science, The University of Manchester, Manchester, UK

    Renate A. Schmidt

Rights and permissions

Reprints and permissions

Copyright information

© 2009 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Swiderski, S., Parting, M., Giesl, J., Fuhs, C., Schneider-Kamp, P. (2009). Termination Analysis by Dependency Pairs and Inductive Theorem Proving. In: Schmidt, R.A. (eds) Automated Deduction – CADE-22. CADE 2009. Lecture Notes in Computer Science(), vol 5663. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-02959-2_25

Download citation

  • DOI: https://doi.org/10.1007/978-3-642-02959-2_25

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-642-02958-5

  • Online ISBN: 978-3-642-02959-2

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation