47 Pages
English

HIGHER ORDER HORN CLAUSES

-

Gain access to the library to view online
Learn more

Description

Niveau: Supérieur, Doctorat, Bac+8
HIGHER-ORDER HORN CLAUSES GOPALAN NADATHUR Duke University, Durham, North Carolina DALE MILLER University of Pennsylvania, Philadelphia, Pennsylvania Abstract: A generalization of Horn clauses to a higher-order logic is described and ex- amined 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 con- text 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 re- sults have a practical realization in the higher-order logic programming language called ?Prolog. Categories and Subject Descriptors: D.3.1 [Programming Languages]: Formal Defi- nitions and Theory — syntax; F.4.1 [Mathematical Logic and Formal Languages]: Mathematical Logic — logic programming; I.

  • quantification over

  • theoretic discussions

  • predicate variable

  • interweaves higher

  • programming

  • logic programming

  • higher-order logic

  • order horn

  • various higher order


Subjects

Informations

Published by
Reads 61
Language English
HIGHER-ORDER HORN CLAUSES
GOPALAN NADATHUR Duke University, Durham, North Carolina
DALE MILLER University of Pennsylvania, Philadelphia, Pennsylvania
Abstract: A generalization of Horn clauses to a higher-order logic is described and ex-amined as a basis for logic programming. In qualitative terms, these higher-order Horn clauses are obtained from the rst-order ones by replacing rst-order terms with simply typedλby permitting quantication over all occurrences of function symbols-terms and 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 con-text 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 rst-order Horn clauses. A complete theorem proving procedure is also described for the extension. This procedure is obtained by interweaving higher-order unication with backchaining and goal reductions, and constitutes a higher-order generalization of SLD-resolution. These re-sults have a practical realization in the higher-order logic programming language called λProlog.
Categories and Subject Descriptors: D.3.1 [Programming Languages De-]: Formal nitions and Theory — syntax; F.4.1 [Mathematical Logic and Formal Languages]: Mathematical Logic — logic programming; I.2.3 [Articial Intelligence and]: Deduction Theorem Proving — logic programming
General Terms: Languages, Theory
Additional Key Words and Phrases: Higher-order logic, higher-order unication, Horn clauses, Prolog, SLD-resolution
The work of G. Nadathur was funded in part by NSF grant MCS-82-19196 and a Burroughs contract. The work of D. Miller was funded by NSF grant CCR-87-05596 and DARPA grant N000-14-85-K-0018.
Authors’ current addresses: G. Nadathur, Computer Science Department, Duke Univer-sity, Durham, NC 27706; D. Miller, Department of Computer and Information Science, University of Pennsylvania, Philadelphia, PA 19104-6389.
1