Higher-order logic programming

Dale A. Miller; Gopalan Nadathur

doi:10.1007/3-540-16492-8_94

Higher-order logic programming

Dale A. Miller
, Gopalan Nadathur

School of Engineering and Applied Science

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

Abstract

In this paper we consider the problem of extending Prolog to include predicate and function variables and typed λ-terms. For this purpose, we use a higher-order logic to describe a generalization to first-order Horn clauses. We show that this extension possesses certain desirable computational properties. Specifically, we show that the familiar operational and least fixpoint semantics can be given to these clauses. A language, λProlog that is based on this generalization is then presented, and several examples of its use are provided. We also discuss an interpreter for this language in which new sources of branching and backtracking must be accommodated. An experimental interpreter has been constructed for the language, and all the examples in this paper have been tested using it.

Original language	English
Title of host publication	3rd International Conference on Logic Programming - Imperial College of Science and Technology, Proceedings
Editors	Ehud Shapiro
Publisher	Springer Verlag
Pages	448-462
Number of pages	15
ISBN (Print)	9783540164920
DOIs	https://doi.org/10.1007/3-540-16492-8_94
Publication status	Published - 1 Jan 1986
Externally published	Yes
Event	3rd International Conference on Logic Programming, ICLP 1986 - London, United Kingdom Duration: 14 Jul 1986 → 18 Jul 1986

Publication series

Name	Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume	225 LNCS
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

Conference

Conference	3rd International Conference on Logic Programming, ICLP 1986
Country/Territory	United Kingdom
City	London
Period	14/07/86 → 18/07/86

Access to Document

10.1007/3-540-16492-8_94

Cite this

Miller, D. A., & Nadathur, G. (1986). Higher-order logic programming. In E. Shapiro (Ed.), 3rd International Conference on Logic Programming - Imperial College of Science and Technology, Proceedings (pp. 448-462). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 225 LNCS). Springer Verlag. https://doi.org/10.1007/3-540-16492-8_94

Miller, Dale A. ; Nadathur, Gopalan. / Higher-order logic programming. 3rd International Conference on Logic Programming - Imperial College of Science and Technology, Proceedings. editor / Ehud Shapiro. Springer Verlag, 1986. pp. 448-462 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).

@inproceedings{9d3a74a3210a40f28b9edd8e338a8a1c,

title = "Higher-order logic programming",

abstract = "In this paper we consider the problem of extending Prolog to include predicate and function variables and typed λ-terms. For this purpose, we use a higher-order logic to describe a generalization to first-order Horn clauses. We show that this extension possesses certain desirable computational properties. Specifically, we show that the familiar operational and least fixpoint semantics can be given to these clauses. A language, λProlog that is based on this generalization is then presented, and several examples of its use are provided. We also discuss an interpreter for this language in which new sources of branching and backtracking must be accommodated. An experimental interpreter has been constructed for the language, and all the examples in this paper have been tested using it.",

author = "Miller, \{Dale A.\} and Gopalan Nadathur",

note = "Publisher Copyright: {\textcopyright} 1986, Springer-Verlag.; 3rd International Conference on Logic Programming, ICLP 1986 ; Conference date: 14-07-1986 Through 18-07-1986",

year = "1986",

month = jan,

day = "1",

doi = "10.1007/3-540-16492-8\_94",

language = "English",

isbn = "9783540164920",

series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

publisher = "Springer Verlag",

pages = "448--462",

editor = "Ehud Shapiro",

booktitle = "3rd International Conference on Logic Programming - Imperial College of Science and Technology, Proceedings",

}

Miller, DA & Nadathur, G 1986, Higher-order logic programming. in E Shapiro (ed.), 3rd International Conference on Logic Programming - Imperial College of Science and Technology, Proceedings. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 225 LNCS, Springer Verlag, pp. 448-462, 3rd International Conference on Logic Programming, ICLP 1986, London, United Kingdom, 14/07/86. https://doi.org/10.1007/3-540-16492-8_94

Higher-order logic programming. / Miller, Dale A.; Nadathur, Gopalan.
3rd International Conference on Logic Programming - Imperial College of Science and Technology, Proceedings. ed. / Ehud Shapiro. Springer Verlag, 1986. p. 448-462 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 225 LNCS).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

TY - GEN

T1 - Higher-order logic programming

AU - Miller, Dale A.

AU - Nadathur, Gopalan

PY - 1986/1/1

Y1 - 1986/1/1

N2 - In this paper we consider the problem of extending Prolog to include predicate and function variables and typed λ-terms. For this purpose, we use a higher-order logic to describe a generalization to first-order Horn clauses. We show that this extension possesses certain desirable computational properties. Specifically, we show that the familiar operational and least fixpoint semantics can be given to these clauses. A language, λProlog that is based on this generalization is then presented, and several examples of its use are provided. We also discuss an interpreter for this language in which new sources of branching and backtracking must be accommodated. An experimental interpreter has been constructed for the language, and all the examples in this paper have been tested using it.

AB - In this paper we consider the problem of extending Prolog to include predicate and function variables and typed λ-terms. For this purpose, we use a higher-order logic to describe a generalization to first-order Horn clauses. We show that this extension possesses certain desirable computational properties. Specifically, we show that the familiar operational and least fixpoint semantics can be given to these clauses. A language, λProlog that is based on this generalization is then presented, and several examples of its use are provided. We also discuss an interpreter for this language in which new sources of branching and backtracking must be accommodated. An experimental interpreter has been constructed for the language, and all the examples in this paper have been tested using it.

U2 - 10.1007/3-540-16492-8_94

DO - 10.1007/3-540-16492-8_94

M3 - Conference contribution

AN - SCOPUS:84976835681

SN - 9783540164920

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 448

EP - 462

BT - 3rd International Conference on Logic Programming - Imperial College of Science and Technology, Proceedings

A2 - Shapiro, Ehud

PB - Springer Verlag

T2 - 3rd International Conference on Logic Programming, ICLP 1986

Y2 - 14 July 1986 through 18 July 1986

ER -

Miller DA, Nadathur G. Higher-order logic programming. In Shapiro E, editor, 3rd International Conference on Logic Programming - Imperial College of Science and Technology, Proceedings. Springer Verlag. 1986. p. 448-462. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). doi: 10.1007/3-540-16492-8_94

Higher-order logic programming

Abstract

Publication series

Conference

Access to Document

Fingerprint

Cite this