Skip to main content
SpringerLink
Log in

A declarative semantics for the Prolog cut operator

  • Conference paper
  • First Online:
Extensions of Logic Programming (ELP 1996)

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

Included in the following conference series:

Abstract

In practice, a large part of most Prolog programs is in fact functional, the search facilities of Prolog are only rarely needed. In order to arrive at efficient implementations it is then convenient to make use of the cut operator provided by Prolog. Up to now, this operator has been regarded as an extra-logical control operator that destroys the declarative semantics of Prolog. In this paper we will show that this is not true. If the cut is used to implement functional predicates and if, furthermore, a certain discipline in its use is adhered to, then programs using the cut operator do possess a declarative semantics.

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 Sandro Etalle. On the unification free Prolog programs. In S. Sokolowski, editor, Proceedings of the Conference on Mathematical Foundations of Computer Science (MFCS '93), Lecture Notes in Computer Science. Springer Verlag, 1993. Available at: http://www.cwi.nl/cwi/publications/index.html.

    Google Scholar 

  2. James Andrews. The logical semantics of the prolog cut. In John W. Lloyd, editor, International Logic Programming Symposium '95. MIT, 1995.

    Google Scholar 

  3. Krzysztof R. Apt. Logic programming. In J. van Leeuwen, editor, Handbook of Theoretical Computer Science, Volume B, chapter 10, pages 495–574. Elsevier, 1990.

    Google Scholar 

  4. Krzysztof R. Apt, editor. Logic Programming. The MIT Press, 1992.

    Google Scholar 

  5. Krzysztof R. Apt. Declarative programming in Prolog. In D. Miller, editor, Proceedings of International Logic Programming Symposium (ILPS '93), Cambridge, Mass./London, 1993. The MIT Press. Available at: http://www.cwi.nl/cwi/publications/index.html.

    Google Scholar 

  6. L. Bachmair and H. Ganzinger. Rewrite-based equational theorem proving with selection and simplification. Journal of Logic and Computation, 4(3):217–247, 1994.

    Google Scholar 

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

  8. E. Börger. A logical operational semantics of full Prolog, part I: Selection core and control. In E. Börger, H. Kleine Büning, and M. M. Richter, editors, Computer Science Logic CSL '89, pages 36–64. Springer-Verlag, Lecture Notes in Computer Science 440, 1989.

    Google Scholar 

  9. Adel Bouhoula. SPIKE: a system for sufficient completeness and parameterized inductive proofs. In Alan Bundy, editor, Twelfth International Conference on Automated Deduction, LNAI 814, pages 836–840, Nancy, France, 1994. Springer-Verlag.

    Google Scholar 

  10. Adel Bouhoula and Michaël Rusinowitch. Implicit induction in conditional theories. Journal of Automated Reasoning, 1995.

    Google Scholar 

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

  12. A. de Bruin and E.P. de Vink. Continuation semantics for Prolog with cut. In Theory and practice of software engineering, volume 351 of Lecture Notes in Computer Science, pages 178–192. Springer-Verlag, 1989.

    Google Scholar 

  13. P. Dembinski and J. Maluszynski. And-parallelism with intelligent back-tracking for annotated logic programs. In Proceedings of the International Symposium on Logic Programming, 1985.

    Google Scholar 

  14. Fergus Henderson, Zoltan Somogyi, and Thomas Conway. Determinism analysis in the mercury compiler. In Proceedings of the Australian Computer Science Conference, 1996. Available at: http://www.cs.mu.oz.au/∼zs/mercury/papers.html.

    Google Scholar 

  15. N. D. Jones and A. Mycroft. Stepwise development of operational and denotational semantics for prolog. In 1984 International Symposium on Logic Programming, pages 281–288. IEEE, 1984.

    Google Scholar 

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

    Google Scholar 

  17. J.-L. Lassez and M. J. Maher. Unification revisited. In J. Minker, editor, Foundations of Deductive Databases and Logic Programming, pages 587–625. Morgan Kaufmann, Los Altos, 1987.

    Google Scholar 

  18. Alan Mycroft and Richard A. O'Keefe. A polymorphic type system for Prolog. Artificial Intelligence, 23:295–307, 1984.

    Google Scholar 

  19. Martin Müller. Automatisierbare Terminierungsnachweise von Prolog-Programmen. Master's thesis, Universität Marburg, 1995. Available at: http://www.mathematik.uni-marburg.de/∼mueller/termnach.ps.

    Google Scholar 

  20. Andreas Podelski and Gert Smolka. Operational semantics of constraint logic programs with coroutining. In Leon Sterling, editor, Proceedings of the 1995 International Conference on Logic Programming, pages 449–463, Kanagawa, Japan, 13–18 June 1995. The MIT Press.

    Google Scholar 

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

  22. Zoltan Somogyi, Fergus Henderson, and Thomas Conway. Logic programming for the real world. 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 83–94, 1995. The Proceedings of this workshop are available at: ftp://ps-ftp.dfki.uni-sb.de/pub/ILPS95-FutureLP/.

    Google Scholar 

  23. Robert F. Stärk. Formal methods for logic programming systems. Technical report, Department of Mathematics, Stanford University, 1995. Available at: http://www-leland.stanford.edu/∼staerk/list.html.

    Google Scholar 

  24. Robert F. Stärk. Total correctness of pure Prolog programs: A formal approach. In Roy Dyckhoff, Heinrich Herre, and Peter Schroeder-Heister, editors, Fifth International Workshop on Extensions of Logic Programming (ELP '96), Lecture Notes in Computer Science. Springer-Verlag, 1996.

    Google Scholar 

  25. Karl Stroetmann. Seduct — a proof compiler for first order logic. In Manfred Broy and Stefan Jänichen, editors, KORSO: Methods, Languages, and Tools for the Construction of Correct Software, volume 1009 of Lecture Notes in Computer Science. Springer Verlag, 1995.

    Google Scholar 

  26. Paul J. Voda. The logical reconstruction of cuts as one solution operators. In John W. Lloyd, editor, Proceedings of the Workshop on Meta-programming in Logic Programming, pages 379–384. 1988.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Corporate Research and Development, Siemens AG, 81730, Munich

    Karl Stroetmann & Thomas Glaß

Authors
  1. Karl Stroetmann
    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

Corresponding author

Correspondence to Karl Stroetmann .

Editor information

Roy Dyckhoff Heinrich Herre Peter Schroeder-Heister

Rights and permissions

Reprints and permissions

Copyright information

© 1996 Springer-Verlag

About this paper

Cite this paper

Stroetmann, K., Glaß, T. (1996). A declarative semantics for the Prolog cut operator. In: Dyckhoff, R., Herre, H., Schroeder-Heister, P. (eds) Extensions of Logic Programming. ELP 1996. Lecture Notes in Computer Science, vol 1050. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-60983-0_18

Download citation

  • DOI: https://doi.org/10.1007/3-540-60983-0_18

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-60983-4

  • Online ISBN: 978-3-540-49751-6

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation