Skip to main content
SpringerLink
Log in

Proving termination of general Prolog programs

  • Conference paper
  • First Online:
Theoretical Aspects of Computer Software (TACS 1991)

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

Included in the following conference series:

Abstract

We study here termination of general logic programs with the Prolog selection rule. To this end we extend the approach of Apt and Pedreschi [AP90] and consider the class of left terminating general programs. These are general logic programs that terminate with the Prolog selection rule for all ground goals. We introduce the notion of an acceptable program and prove that acceptable programs are left terminating. This provides us with a practical method of proving termination.

The converse implication does not hold but we show that under the assumption of non-floundering from ground goals every left terminating program is acceptable. Finally, we prove that various ways of defining semantics coincide for acceptable programs. The method is illustrated by giving simple proofs of termination of a “game” program and the transitive closure program for the desired class of goals.

Note. First author's work was partly supported by ESPRIT Basic Research Action 3020 (Integration). Second author's work was partly supported by ESPRIT Basic Research Action 3012 (Compulog).

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.

Similar content being viewed by others

References

  1. K. R. Apt and M. Bezem. Acyclic programs. In D. H. D. Warren and P. Szeredi, editors, Proceedings of the Seventh International Conference on Logic Programming, pages 617–633. The MIT Press, 1990.

    Google Scholar 

  2. K. R. Apt, H. A. Blair, and A. Walker. Towards a theory of declarative knowledge. In J. Minker, editor, Foundations of Deductive Databases and Logic Programming, pages 89–148. Morgan Kaufmann, 1988.

    Google Scholar 

  3. K. R. Apt and D. Pedreschi. Studies in pure Prolog: termination. In J.W. Lloyd, editor, Symposium on Computional Logic, pages 150–176, Berlin, 1990. Springer-Verlag.

    Google Scholar 

  4. K. R. Apt. Logic programming. In J. van Leeuwen, editor, Handbook of Theoretical Computer Science, pages 493–574. Elsevier, 1990. Vol. B.

    Google Scholar 

  5. M. Baudinet. Proving termination properties of PROLOG programs. In Proceedings of the 3rd Annual Symposium on Logic in Computer Science (LICS), pages 336–347, Edinburgh, Scotland, 1988.

    Google Scholar 

  6. M. Bezem. Characterizing termination of logic programs with level mappings. In E. L. Lusk and R. A. Overbeek, editors, Proceedings of the North American Conference on Logic Programming, pages 69–80. The MIT Press, 1989.

    Google Scholar 

  7. L. Cavedon. Continuity, consistency, and completeness properties for logic programs. In G. Levi and M. Martelli, editors, Proceedings of the Sixth International Conference on Logic Programming, pages 571–584. The MIT Press, 1989.

    Google Scholar 

  8. N. Dershowitz. Termination of rewriting. Journal of Symbolic Computation, 8:69–116, 1987.

    Google Scholar 

  9. M. Fitting. A Kripke-Kleene semantics for general logic programs. Journal of Logic Programming, 2:295–312, 1985.

    Article  Google Scholar 

  10. S. Hanks and D. McDermott. Nonmonotonic logic and temporal projection. Artificial Intelligence, 33:379–412, 1987.

    Google Scholar 

  11. S. C. Kleene. Introduction to Metamathematics. van Nostrand, New York, 1952.

    Google Scholar 

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

    Google Scholar 

  13. L. Plümer. Termination Proofs for Logic Programs. Lecture Notes in Artificial Intelligence 446, Springer-Verlag, Berlin, 1990.

    Google Scholar 

  14. L. Plümer. Termination proofs for logic programs based on predicate inequalities. In D. H. D. Warren and P. Szeredi, editors, Proceedings of the Seventh International Conference on Logic Programming, pages 634–648. The MIT Press, 1990.

    Google Scholar 

  15. J. D. Ullman and A. van Gelder. Efficient tests for top-down termination of logical rules. J. ACM, 35(2):345–373, 1988.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Centre for Mathematics and Computer Science, Kruislaan 413, 1098 SJ, Amsterdam, The Netherlands

    Krzysztof R. Apt

  2. Dipartimento di Informatica, Università di Pisa, Corso Italia 40, 56125, Pisa, Italy

    Dino Pedreschi

Authors
  1. Krzysztof R. Apt
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Dino Pedreschi
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Takayasu Ito Albert R. Meyer

Rights and permissions

Reprints and permissions

Copyright information

© 1991 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Apt, K.R., Pedreschi, D. (1991). Proving termination of general Prolog programs. In: Ito, T., Meyer, A.R. (eds) Theoretical Aspects of Computer Software. TACS 1991. Lecture Notes in Computer Science, vol 526. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-54415-1_50

Download citation

  • DOI: https://doi.org/10.1007/3-540-54415-1_50

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-54415-9

  • Online ISBN: 978-3-540-47617-7

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation