Theory of logic programming. An elementary introduction (Q1202019)

This is a carefully written textbook on Horn clause logic for graduate students of mathematics or of theoretical computer science. While no specific mathematical prerequisites are necessary for studying the book, the general level of presentation is very high. Each chapter contains a short synopsis and concludes with a guide to the recent research literature. Complete proofs of all major theorems are given and exercises with selected solutions are provided. After a brief introduction into the predicate calculus, the author discusses Herbrand models for sets of universal sentences; then unification and resolution are introduced in order to prove the various completeness theorems for ``prolog situations''. The book is organized along the lines of \textit{Lloyds} classic ``Foundations of Logic Programming'' [\textit{J. W Lloyd}, Foundation of Logic Programming, 2nd ext. ed., Springer-Verlag, Berlin (1987; Zbl 0668.68004)], but contains additional material on 3-valued logic and generalized Prolog situations. There is also a final chapter on constraint logic programming. Readers familiar with universal algebra and model theory may find the sections on saturated structures and Malcev's characterization of Horn classes quite illuminating.