Tim@CIS.UPENN.EDU.UUCP (12/03/86)
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.
2:30 pm December 5, 1986
Room 23, Moore School
University of Pennsyulvania
Thesis Supervisor: Dale Miller
Committee: Tim Finin, Jean Gallier (Chairman), Andre Scedrov, Richard Statman