zbMATH — the first resource for mathematics

Foundations of logic programming. (English) Zbl 0547.68005
Symbolic Computation. Artificial Intelligence. Berlin etc.: Springer- Verlag. X, 124 p. DM 49.00 (1984).
This book is an attempt to present, in a unified manner, a field of major importance for computer science and artificial intelligence: the theoretical bases of logic programming languages, including, in particular, PROLOG. The fundamental idea that logic can be used as a programming language and the effort to use this idea in the design of the new generations of computers, gave rise to an extraordinary effervescence of research on this direction. Old results are reconsidered, new results complete the work. The most important mathematical tools used, at least in the present book, are: fixed-point theory, model theory, unification and resolution procedures, infinite computation processes within the frame of discrete (metric) topological spaces, etc.
The matter of the four chapters could be sketched as follows: Chapter I presents the declarative semantics of logic programs. The concepts of (correct) answer substitution is introduced, the fixed-point characterization of the least Herbrand model is given and the conditions within the correctness of an answer substitution is equivalent with the interpretation of a program in its least Herbrand model are specified.
Chapter II is concerned with procedural semantics of logic programs. The declarative concepts are implemented using the SLD-resolution (Linear resolution with Selection function for Definite clauses). The soundness and completeness of SLD-resolution and the independence of the computation rule are the main results of the chapter. SLD-refutation procedures are discussed and it is argued that (PROLOG) cuts can introduce a form of incompleteness into the SLD-resolution implementation of correct answer substitution.
Chapter III is dealing with negation. The finite failure set of a program is introduced and its relations to the (non-monotonic) inference rules of the closed world assumption and negation as failure rule are explored. SLD-resolution is a sound and complete implementation of the finite failure. The completion of a general program is defined, the definition of the correct answer substitution is extended to the completion of a general program. The soundness and completeness results of the negation as failure rule are proved. The correct implementation of the negation rules in PROLOG systems is discussed.
Chapter IV tries to offer a generalized formal frame to the behaviour of programs which do not terminate and yet are doing useful computation (perpetual processes). Generalized notions are needed: complete Herbrand universe, base and model. Properties of these notions on topological (metric) spaces are elegantly deduced and the soundness of SLD-resolution for infinite computations is shown using the set of all atoms ”computable at infinity”.
The book represents an original pioneering synthesis in a field of interest for computer science future development and it is sure that, according to the present research efforts, it will be followed by similar extended approaches.
Reviewer: N.Curteanu

68-02 Research exposition (monographs, survey articles) pertaining to computer science
68N01 General topics in the theory of software
68Q65 Abstract data types; algebraic specification
68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)
68W30 Symbolic computation and algebraic computation
03B35 Mechanization of proofs and logical operations
68Q60 Specification and verification (program logics, model checking, etc.)
03C99 Model theory