HIGHER ORDER HORN CLAUSES

Duke University

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

Sujets

• University
• Predicate variable
• Computer programming
• Logic programming
• Higher-order logic

Informations

• Publié par: profil-zyak-2012
• Nombre de lectures: 61
• Langue: English

Extrait

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