Thumbnail
Access Restriction
Subscribed

Author Nadathur, Gopalan ♦ Miller, Dale
Source ACM Digital Library
Content type Text
Publisher Association for Computing Machinery (ACM)
File Format PDF
Copyright Year ©1990
Language English
Subject Domain (in DDC) Computer science, information & general works ♦ Data processing & computer science
Abstract 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.
ISSN 00045411
Age Range 18 to 22 years ♦ above 22 year
Educational Use Research
Education Level UG and PG
Learning Resource Type Article
Publisher Date 1990-10-01
Publisher Place New York
e-ISSN 1557735X
Journal Journal of the ACM (JACM)
Volume Number 37
Issue Number 4
Page Count 38
Starting Page 777
Ending Page 814


Open content in new tab

   Open content in new tab
Source: ACM Digital Library