Skip to main content
SpringerLink
Log in

Automated modular termination proofs for real Prolog programs

  • Contributed Papers
  • Conference paper
  • First Online:
Static Analysis (SAS 1996)

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 1145))

Included in the following conference series:

Abstract

We present a methodology for checking the termination of Prolog programs that can be automated and is scalable. Furthermore, the proposed method can be used to locate errors. It has been successfully implemented as part of a tool that uses static analysis based on formal methods in order to validate Prolog programs. This tool is aimed at supporting the design and maintenance of Prolog programs.

Our approach is based on a natural extension of the notion of acceptable programs developed in Apt and Pedreschi [AP90, AP93]. The main idea is to assign a measure of complexity to predicate calls. Then the termination of a program is shown by proving this measure to be decreasing on recursive calls. While this measure is a natural number in [AP90, AP93], we extend this idea by using tuples of natural numbers as a measure of complexity. These tuples are compared lexicographicly. The use of this kind of measure enables us to refine the notion of acceptable programs to the notion of loop free programs. This notion can be used to modularize the termination proof of Prolog programs to a greater extend than previously possible.

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

Access this chapter

Log in via an institution

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Krzysztof R. Apt and Elena Marchiori. Reasoning about Prolog programs: From modes through types to assertions. Formal Aspects of Computing, 6A:743–764, 1994.

    Google Scholar 

  2. Krzysztof R. Apt and Dino Pedreschi. Studies in pure Prolog: Termination. In John W. Lloyd, editor, Symposium on Computational Logic, pages 150–176. Springer-Verlag, 1990.

    Google Scholar 

  3. Krysztof R. Apt and Dino Pedreschi. Modular termination proofs for logic and pure prolog programs. In G. Levi, editor, Proceedings of Fourth International School for Computer Science Researchers. Oxford University Press, 1993.

    Google Scholar 

  4. Krzysztof R. Apt, editor. Proceedings of the Joint International Conference and Symposium on Logic Programming, Washington, D. C., USA, November, 9–13 1992. The MIT Press.

    Google Scholar 

  5. Jürgen Avenhaus. Reduktionssysteme — Rechnen und SchlieΒen in gleichungsdefinierten Strukturen, Springer-Verlag, 1995.

    Google Scholar 

  6. Leo Bachmair. Canonical Equational Proofs. Birkhäuser Boston, Inc., Boston, MA, 1991.

    Google Scholar 

  7. Bossi, Coco, and Fabris. Norms on terms and their use in proving universal termination of a logic program. Theoretical Computer Science, 124,2:297–328, 1994.

    Google Scholar 

  8. Marc Bezem. Characterizing termination of logic programs with level mappings. In Ewing L. Lusk and Ross A. Qverbeek, editors, Logic Programming, Proceedings of the North American Conference, volume 1, pages 69–80, Cleveland, Ohio, USA, October 16–20, 1989. The MIT Press, Cambridge, Massachusetts.

    Google Scholar 

  9. Marc Bezem. Strong termination of logic programs. Journal of Logic Programming, 15(1&2):79–98, 1993.

    Google Scholar 

  10. W. W. Bledsoe. A new method for proving Presburger formulas. In 4th International Joint Conference on Artificial Intelligence, September 1975. Tibilisi, Georgia, U.S.S.R.

    Google Scholar 

  11. FranÇois Bronsard, T. K. Lakshman, and Uday S. Reddy. A framework of directionality for proving termination of logic programs. In Apt [Apt92], pages 321–335.

    Google Scholar 

  12. K. L. Clark. Negation as failure. In H. Gallaire and J. Minker, editors, Logic and Data Bases, pages 293–322. Plenum Press, New York, 1978.

    Google Scholar 

  13. P. Deransart, A. A. Ed-Dbali, and L. Cervoni. Prolog: The Standard. Springer-Verlag, 1996.

    Google Scholar 

  14. Herbert B. Enderton. A Mathematical Introduction to Logic. Academic Press, 1972.

    Google Scholar 

  15. Gerhard Gröger and Lutz Plümer. Handling of mutual recursion in automatic termination proofs for logic programs. In Apt [Apt92], pages 336–350.

    Google Scholar 

  16. P. M. Hill and R. W. Topor. A semantics for typed logic programs. In Pfenning [Pfe92], pages 1–62.

    Google Scholar 

  17. J. W. Lloyd. Foundations of Logic Programming. Springer-Verlag, Berlin, second edition, 1987.

    Google Scholar 

  18. Mascellani and Pedreschi. Proving termination of prolog programs. In M. Alpuente, R. Barbuti, and I. Ramos, editors, Proceedings of GULPPRODE'94, Joint conference on declarative programming, pages 46–61, 1994.

    Google Scholar 

  19. Frank Pfenning, editor. Types in Logic Programming. MIT, Cambridge, Mass./London, 1992.

    Google Scholar 

  20. Wolfram Pohlers. Proof Theory. An Introduction. Number 1407 in Lecture Notes in Mathematics. Springer-Verlag, Berlin/Heidelberg/New York, 1989.

    Google Scholar 

  21. M. Presburger. über die Vollständigkeit eines gewissen Systems der Arithmetik ganzer Zahlen, in welchem die Addition als einzige Operation hervortritt. Sprawozdanie z I Kongrescu Matematykow Krajow Slowkanskich Warszawa, pages 92–101, 1929.

    Google Scholar 

  22. Karl Stroetmann and Thomas Glaß. Augmented PROLOG — An evolutionary approach. In Donald A. Smith, Olivier Ridoux, and Peter Van Roy, editors, Proceedings of the Workshop Visions for the Future of Logic Programming: Laying the Foundations for a Modern Successor to Prolog, pages 59–70, 1995. The Proceedings of this workshop are available at: ftp://ps-ftp.dfki.uni-sb.de/pub/ILPS95-FutureLP/.

    Google Scholar 

  23. Karl Stroetmann, Thomas Glaß, and Martin Müller. Implementing safetycritical systems in Prolog: Experiences from the R&D at Siemens. In Peter Reintjes, editor, Practical Applications of Prolog '96, pages 391–403, 1996.

    Google Scholar 

  24. D. De Schreye, Kristof Verschaetse, and Maurice Bruynooghe. A frame-work for analysing the termination of definite logic programs with respect to call patterns. In Proceedings of the International Conference on Fifth Generation Computer Systems, pages 481–488. ICOT, 1992.

    Google Scholar 

  25. Christoph Walther. Automatisierung von Terminierungsbeweisen. Vieweg, Braunschweig, Germany, 1990.

    Google Scholar 

  26. Eyal Yardeni, Thom Frühwirth, and Ehud Shapiro. Polymorphically typed logic programs. In Pfenning [Pfe92], pages 63–90.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Siemens AG ZT SE 1, D-81730, München, Germany

    Martin Müller, Thomas Glaß & Karl Stroetmann

Authors
  1. Martin Müller
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Thomas Glaß
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Karl Stroetmann
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Radhia Cousot David A. Schmidt

Rights and permissions

Reprints and permissions

Copyright information

© 1996 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Müller, M., Glaß, T., Stroetmann, K. (1996). Automated modular termination proofs for real Prolog programs. In: Cousot, R., Schmidt, D.A. (eds) Static Analysis. SAS 1996. Lecture Notes in Computer Science, vol 1145. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-61739-6_44

Download citation

  • DOI: https://doi.org/10.1007/3-540-61739-6_44

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-61739-6

  • Online ISBN: 978-3-540-70674-8

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation