Higher-Order Horn Clauses

Gopalan Nadathur, Dale Miller

Research output: Contribution to journalArticlepeer-review

64 Scopus citations


A generalization of Horn clauses to a higher-order logic is described and examined as a basis for logic programming. In qualitative terms, these higher-order Horn clauses are obtained from the first-order ones by replacing first-order terms with simply typed λ-terms and by permitting quantification over all occurrences of function symbols and some occurrences of predicate symbols. Several proof-theoretic results concerning these extended clauses are presented. One result shows that although the substitutions for predicate variables can be quite complex in general, the substitutions necessary in the context of higher-order Horn clauses are tightly constrained. This observation is used to show that these higher-order formulas can specify computations in a fashion similar to first-order Horn clauses. A complete theorem-proving procedure is also described for the extension. This procedure is obtained by interweaving higher-order unification with backchaining and goal reductions, and constitutes a higher-order generalization of SLD-resolution. These results have a practical realization in the higher-order logic programming language called λProlog.

Original languageEnglish (US)
Pages (from-to)777-814
Number of pages38
JournalJournal of the ACM (JACM)
Issue number4
StatePublished - Jan 10 1990


Dive into the research topics of 'Higher-Order Horn Clauses'. Together they form a unique fingerprint.

Cite this