Get 20M+ Full-Text Papers For Less Than $1.50/day. Subscribe now for You or Your Team.

Learn More →

Higher-order Horn clauses

Higher-order Horn clauses Higher-Order GOPALAN Duke University, Horn Clauses NADATHUR Durham, North Carolina AND DALE University MILLER of Pennsylvania, Philadelphia, Pennsylvania 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 tirstorder ones by replacing first-order terms with simply typed X-terms and by permitting quantification over all occurrences of function symbols and some occurrences of predicate symbols. Several prooftheoretic 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 higherorder generalization of SLD-resolution. These results have a practical realization in the higher-order logic programming language called XProlog. Categories and Subject Descriptors: D.3.1 [Programming Languages]: Formal Definitions and Theorysyntax; F.4.1 [Mathematical Logic and Formal Languages]: Mathematical Logic--logic programming; http://www.deepdyve.com/assets/images/DeepDyve-Logo-lg.png Journal of the ACM (JACM) Association for Computing Machinery

Loading next page...
 
/lp/association-for-computing-machinery/higher-order-horn-clauses-r4KyT150cY

References

References for this paper are not available at this time. We will be adding them shortly, thank you for your patience.

Publisher
Association for Computing Machinery
Copyright
Copyright © 1990 by ACM Inc.
ISSN
0004-5411
DOI
10.1145/96559.96570
Publisher site
See Article on Publisher Site

Abstract

Higher-Order GOPALAN Duke University, Horn Clauses NADATHUR Durham, North Carolina AND DALE University MILLER of Pennsylvania, Philadelphia, Pennsylvania 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 tirstorder ones by replacing first-order terms with simply typed X-terms and by permitting quantification over all occurrences of function symbols and some occurrences of predicate symbols. Several prooftheoretic 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 higherorder generalization of SLD-resolution. These results have a practical realization in the higher-order logic programming language called XProlog. Categories and Subject Descriptors: D.3.1 [Programming Languages]: Formal Definitions and Theorysyntax; F.4.1 [Mathematical Logic and Formal Languages]: Mathematical Logic--logic programming;

Journal

Journal of the ACM (JACM)Association for Computing Machinery

Published: Oct 1, 1990

References