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

Lassez, J.-L.; Maher, M. J.

Theor. Comput. Sci. 30, 167-184 (1984).

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

MSC:

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

Keywords:

SLD resolution; logic programs; fixed point theorems; denotational semantics

Citations:

Zbl 0483.68004

References:

[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)