Closures and fairness in the semantics of programming logic. (English) Zbl 0547.68034

Using the techniques of closures and chaotic iterations of P. Cousot and R. Cousot, the authors give a semantics to logic programs and then study some fixed point theorems, denotational semantics and the like. The final section is devoted to an extension of the characterization of SLD finite failure given by K. R. Apt and M. H. van Emden [J. Assoc. Comput. Mach. 29, 841-862 (1982; Zbl 0483.68004)].
Reviewer: H.Nishimura


68Q65 Abstract data types; algebraic specification
68N01 General topics in the theory of software
68Q60 Specification and verification (program logics, model checking, etc.)


Zbl 0483.68004
Full Text: DOI


[1] Apt, K. R.; van Emden, M. H., Contributions to the theory of logic programming, J. ACM, 29, 841-862 (1982) · Zbl 0483.68004
[2] Clark, K. L., Negation as failure, (Gallaire, H.; Minker, J., Logic and Data Bases (1978), Plenum Press: Plenum Press New York), 293-324
[3] Colmerauer, A., Prolog II manuel de référence et modèle, théorique, (Rapp. Rech. GIA ERA CNRS, 363 (1982), Université Aix-Marseille II)
[4] Cousot, P.; Cousot, R., Automatic synthesis of optimal invariant assertions: Mathematical foundations, ACM Symp. on Artificial Intelligence and Programming Languages; SIGPLAN Notices, 12, 8, 1-12 (1977)
[5] Cousot, P.; Cousot, R., Constructive versions of Tarski’s fixed point theorems, Pacific J. Math., 82, 1, 43-57 (1979) · Zbl 0413.06004
[6] Cousot, P., Semantic foundations of program analysis, (Muchnick, S. S.; Jones, N. D., Program Flow Analysis: Theory and Application (1981), Prentice-Hall: Prentice-Hall London), 303-342
[7] Van Emden, M. H., Programming with resolution logic, (Elcock, E. W.; Michie, D., Machine Intelligence, Vol. 8 (1977), Ellis Horwood: Ellis Horwood Chichester), 266-299
[8] Van Emden, M. H.; Kowalski, R. A., The semantics of predicate logic as a programming language, J. ACM, 23, 733-742 (1976) · Zbl 0339.68004
[9] Kowalski, R. A., Logic for Problem Solving (1979), Elsevier (North-Holland): Elsevier (North-Holland) New York
[11] Loveland, D. W., Automated Theorem Proving: A Logical Basis (1978), Elsevier (North-Holland): Elsevier (North-Holland) New York · Zbl 0364.68082
[12] Manna, Z., Mathematical Theory of Computation (1974), McGraw-Hill: McGraw-Hill New York · Zbl 0353.68066
[13] Robinson, J. A., A machine-oriented logic based on the resolution principle, J. ACM, 23, 23-41 (1965) · Zbl 0139.12303
[14] Sato, T., Negation and semantics of prolog programs, Proc. 1st Internat. Logic Programming Conf., 169-174 (1982), Marseille, France
[15] Scott, D., Lectures on a mathematical theory of computation, (Tech. Monograph PRG-19 (1981), Programming Research Group, Oxford University) · Zbl 0516.68064
[16] Tarski, A., A lattice-theoretical fixpoint theorem and its applications, Pacific J. Math., 5, 285-309 (1955) · Zbl 0064.26004
[17] Tennent, R. D., Principles of Programming Languages (1981), Prentice-Hall: Prentice-Hall London · Zbl 0463.68008
[18] Wolfram, D. A.; Maher, M. J.; Lassez, J.-L., A unified treatment of resolution strategies for logic programs, (Tech. Rept. 83/12 (1983), Dept. of Computer Science, Univ. of Melbourne)
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.