PROLOG-REQUEST@SU-SCORE.ARPA (Chuck Restivo, The Moderator) (12/03/86)
PROLOG Digest Thursday, 4 Dec 1986 Volume 4 : Issue 81
Today's Topics:
Announcement - Thesis,
LP Library - PDProlog & Update
----------------------------------------------------------------------
Date: Wed, 3 Dec 86 13:14 EST
From: Tim Finin <Tim@cis.upenn.edu>
Subject: Defense
Dissertation Defense
Computer and Information Science
University of Pennsylvania
A HIGHER-ORDER LOGIC AS THE BASIS FOR LOGIC PROGRAMMING
GOPALAN NADATHUR
(gopalan@cis.upenn.edu)
The objective of this thesis is to provide a formal basis for
higher-order features in the paradigm of logic programming. Towards
this end, a non-extensional form of higher-order logic that is based
on Church's simple theory of types is used to provide a generalisation
to the definite clauses of first-order logic. Specifically, a class
of formulas that are called higher-order definite sentences is
described. These formulas extend definite clauses by replacing
first-order terms by the terms of a typed lambda calculus and by
providing for quantification over predicate and function variables.
It is shown that these formulas together with the notion of a proof in
the higher-order logic provide an abstract description of computation
that is akin to the one in the first-order case. While the
construction of a proof in a higher-order logic is often complicated
by the task of finding appropriate substitutions for predicate
variables, it is shown that the necessary substitutions for predicate
variables can be tightly constrained in the context of higher-order
definite sentences. This observation enables the description of a
complete theorem-proving procedure for these formulas. The procedure
constructs proofs essentially by interweaving higher-order unification
with backchaining on implication, and constitutes a generalisation to
the higher-order context of the well-known SLD-resolution procedure
for definite clauses. The results of these investigations are used to
describe a logic programming language called lambda Prolog. This
language contains all the features of a language such as Prolog, and,
in addition, possesses certain higher-order features. The uses of
these additional features are illustrated, and it is shown how the use
of the terms of a (typed) lambda calculus as data structures provides
a source of richness to the logic programming paradigm.
Thesis Supervisor: Dale Miller
Committee: Tim Finin, Jean Gallier (Chairman), Andre Scedrov, Richard
Statman
------------------------------
Date: 7 Nov 86 23:25:46 GMT
From: David Fiore <ucdavis!ucrmath!hope!fiore@ucbvax.Berkeley.EDU>
Subject: PD PROLOG
This is in response to all the letters I have recieved requesting PD
PROLOG. I have had very little luck responding to the letters, much
less getting copies of PD PROLOG to those that wanted it. I am
therefore submitting for the second time a copy of PD PROLOG in
uuencoded format to the Digest.
Good luck with the program!
-- David Fiore
UseNet : ...!ucdavis!ucrmath!hope!fiore
BITNET : consult@ucrvms
------------------------------
Date: Wed 3 Dec 86 11:25:01-PST
From: Chuck Restivo <Restivo@Score.Stanford.EDU>
Subject: PDProlog
[cwr]
I left the following files in SCORE:'s Prolog directory. You'll
need these to use PDProlog.
PS:<PROLOG>
PDPROLOG.CODE.2;P775252 75 189686(7) 3-Dec-86 11:14:13 RESTIVO
.DOCUMENTATION.2;P775252 24 61299(7) 3-Dec-86 11:15:14 RESTIVO
.HELP.1;P775252 1 711(7) 3-Dec-86 11:08:41 RESTIVO
.UUDECODE.2;P775252 3 5560(7) 3-Dec-86 11:18:03 RESTIVO
.UUENCODE.2;P775252 2 4872(7) 3-Dec-86 11:18:59 RESTIVO
-- ed
------------------------------
End of PROLOG Digest
********************