I am reading the book Logic, Programming and Prolog (2nd ed).  After completing the preliminaries chapter, much of the material was familiar since it was defining predicate calculus and logical inferences.  The material is mathematically rigorous by authors Ulf Nilsson and Jan Maluszynski.  They develop a series of definitions to build the language of predicate calculus and inference.  The familiarity was due to my studies from the material presented in Luger and Stubblefield (1992), and Stewart and Norvig (1995).

The authors continue with the SLD-Resolution along with Unification.  They illustrate a unification algorithm as well as proof trees.  Afterwards negation is discussed; thus  they develop the SLDNF-Resolution.  The cut and mathematics is covered.  If used improperly, cuts can make programs unsound and yield false answers.  All this tied into logic programming theory.  The theorems and propostions come from various resources.  The goal of the book is teach programmers on how to write logic programs that are sound, correct, and finite.

I found this book interesting thus far and good introduction to logic programming and prolog.