The higher-order extension to logic programming presented in this research paper attains, within the pure logical basis of the paradigm, the expressive power intended by ad hoc extra-logical metaprogramming or by blending logic programming with functionality. The extension of the paradigm is achieved by replacing first-order terms in the language with \-typed terms and by permitting quantification over function and predicate symbols. These results are the basis for the \Prolog programming language.

After general motivations, the authors discuss the nature of the language involved in the development of the higher-order Horn clauses. They then present a generalization to the class of first-order goal clauses and show that a higher-order provability notion fulfills properties analogous to first-order (Horn) provability. The last step is to provide an SLD-resolution generalization that constitutes the theorem-proving basis for a hypothetical \Prolog interpreter.

This paper is a continuation of the authors’ current research, and researchers in logic programming will find it appealing. Although the work is rather self-contained and the examples are good, some previous context is in order (see Miller and Nadathur [1].) Its length and density will discourage the unfamiliar reader.