Springer Nature is making SARS-CoV-2 and COVID-19 research free. View research | View latest news | Sign up for updates

Two congruent semantics for Prolog with CUT


The development of a formal semantics for a given programming language can proceed in several stages. At each stage we give an alternative semantic definition of the language, and each definition embodies successively more and more implementation details. Then we formulate and prove at each stage the congruence conditions between successive definitions in the sequence. This paper presents two formal semantics for Prolog with “cut” and shows the congruence condition between them.

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


  1. [1]

    J. A. Campbell, (Ed.) Implementations of Prolog, Ellis Horwood Limited, 1984.

  2. [2]

    W. F. Clocksin, and C. S. Mellish, Programming in Prolog, Springer-Verlag, Berlin, 1981.

  3. [3]

    J. A. Goguen, J. W. Thacher, and E. G. Wagner, An Initial Algebra Approach to the Specification, Correctness, and Implementation of Abstract Data Types, Current Trends in Programming Methodology, Vol. IV, Edited by Raymond, T. Yeh, Prentice-Hall, Englewood Cliffs, N. J., 1978.

  4. [4]

    J. V. Guttag, Abstract data types and the development of data structuresCACM,20:6 (1978).

  5. [5]

    R., Kowalski, Predicate Logic as a Programming Language, IFIP74, 569–574.

  6. [6]

    R., Kowalski, Logic for Problem Solving, North-Holland, Amsterdam, 1979.

  7. [7]

    J. F. Nilsson, Formal Vienna-Definition-Method Models of Prolog, Implementations of Prolog, Edited by Campbell, J. A., Ellis Horwood Limited, 1984.

  8. [8]

    J. A., Robinson, A machine-oriented logic based on the resolution principle,JACM,12:1 (1965). 0179 0636 V

  9. [9]

    M.-Y. Zhu, On Specification Language Universe, Proceedings of III CASCO Symposium, Beijing, 1987.

  10. [10]

    M.-Y. Zhu, AUTO STAR—A Software Development System, Technical Report, Beijing Institute of System Engineering, 1988.

  11. [11]

    M.-Y. Zhu, A Prolog Interpreter: A Formal Development with AUTO STAR, Technical Report, Beijing Institute of System Engineering, 1988.

Download references

Author information

Correspondence to Mingyuan Zhu.

Rights and permissions

Reprints and Permissions

About this article

Cite this article

Zhu, M. Two congruent semantics for Prolog with CUT. J. of Comput. Sci. & Technol. 5, 82–91 (1990).

Download citation


  • Bide
  • Formal Semantic
  • Congruent Relation
  • Proof Tree
  • Prolog Program