Foundations of equational logic programming (Q1801319)

This is the most recent of numerous books devoted to the foundations of logic programming appearing over last several years. The book begins with the introductive chapter on history and results in the field, and the preliminary chapter on basic notions and tools, including terms, atoms, equations, substitutions, etc. With these backgrounds at hand the author proceeds to the equational logic programming, exposing its model theory, fixpoint theory, proof theory, unification, resolution and paramodulation. A special chapter is devoted to the universal unification, i.e. a generalized unification when some or all the functions are assumed to be commutative, associative, etc. (that is possess special properties specified via universally quantified equations). As it is well known, there exist at least three ways of handling equations within first order theories. First, by giving an explicit set of first order equality axioms; second, by replacing the unification algorithm with a complete unification procedure in the resolution rule, when we have to find a complete universal unification procedure for a set of axioms we deal with. The third way is based on the application of a new rule in addition to resolution, the so-called paramodulation. However, the search space generated by paramodulation, as is well known, is far too large, and many restrictions or refinements of paramodulation have been proposed. Mainly, these proposals were made in the context of canonical term rewriting systems. For these systems a directed form of paramodulation is complete even being applied only to non-variable terms. But several questions remain. What conditions are needed to use equational clauses only in one direction? Must all variables occurring in the right-hand side of the clause occur also in the left-hand side of it? Can the generalization be made to answer in the above questions positively when dealing with Horn equational theories? The author shows certain restrictions imposed on an equational Horn logic programs to prune the search space. Also he discusses extensively the related rewrite rule techniques, including confluency, narrowing, etc. One chapter of the book is completely devoted to the universal unification by complete sets of transformations, used to compute the most general unifiers for two terms in the presence of additional equational axioms. A major disadvantage of paramodulation is the fact that in a selected subgoal there are, generally, several occurrences to which paramodulation can be applied. Most of these occurrences have to be investigated to guarantee the completeness of the unification procedure. The author proves the completeness of his refutation procedure based on complete sets of transformations. The last chapter of the book discusses the lazy resolution and complete sets of inference rules for Horn equational theories. It is well known that the use of resolution together with various techniques inherits a principal problem. The complete and independent set of unifiers may be infinite or may not even exist. Moreover, the unification problem may be undecidable, even if the equational program is a canonical and unconditional rewrite rule system. Hence, the search space may not only be infinite in depth, but may also be infinite in breadth, and we cannot be sure that the unification procedure will terminate. However, these problems can be solved by using the lazy resolution rule. The strong completeness of complete sets of inference rules together with the lazy resolution is proved. The book is concluded with summary, discussion and posing of remaining open problems. It contains a useful index and extensive bibliography in the field of logic programming. This book is a welcome addition to the literature on the foundations of equational logic programming. It will surely prove useful as a summary of the leading edge in the field, as a reference, and as an adjunct to the earlier books.