*Abstract:* The Logical Framework (LF) is a formal system
for the representation of logics and formal systems as theories
within it, which was developed by Harper, Honsell and Plotkin. The
LF consists of two components: the lambda Pi-calculus, the
lambda-calculus with dependent function space (or product) types;
and the principle of *judgements as types* in which
judgements, the units of inference in logics and other formal
systems, are identified with the types of the lambda Pi-calculus.
This work is strongly influenced by the work of Martin-Löf on
judgements in logic. The LF is suitable for mechanical
implementation because the lambda Pi-calculus is decidable.

We present a theory of search and logic programming for the lambda Pi- calculus and consequently for logics which are adequately represented in the LF.

The presentation of the lambda Pi-calculus of Harper, Honsell and Plotkin is as a (linearized) natural deduction system. The search space induced by such a system is highly non-deterministic and so the first step is to define a Gentzenized system, in which the natural deduction style pi-elimination rule is replaced by a sequent calculus style Pi-elimination rule, which is sound and complete with respect to the system of Harper, Honsell and Plotkin.

The Gentzenized system thus provides the foundation for a
metacalculus, possessing an important subformula property, for the
inhabitation assertions of the lambda Pi-calculus which forms a
suitable basis for proof-search in the lambda Pi-calculus. By
exploiting the structure of a form of *hypothetico-general*
judgement, we are able to obtain (complete) calculi based on
certain forms of resolution rule, the search spaces of which are
properly contained within that of our basic metacalculus.
Furthermore, we are able to further constrain proof-search in these
calculi by considering a certain uniform form for proofs.

We develop a unification algorithm for the lambda Pi-calculus by
extending the work of Huet for the simply-typed lambda-calculus. We
use this unification algorithm to allow us to eliminate
non-deterministic choices of terms, when performing proof-search
with the Pi*l*) or resolution rules. This is done by the
introduction of a class of universal variables which are later
instantiated via the unification algorithm.

When unification is used to instantiate universal variables well-formedness may not be preserved. However, by extending the work of Bibel and Wallen (for first-order classical, modal and intuitionistic logics) to the lambda Pi-calculus we are able to obtain a theory which allows to accept as many such instantiations as possible by detecting when the derivation can be reordered in order to yield a well-formed proof.

We extend the theory described above to provide a notion of
logic programming by admitting universal variables in endsequents:
these are analogous to the *logical variables* of PROLOG .
Finally, we provide a denotational semantics for our logic programs
by performing a least fixed point construction in a collection of
Herbrand interpretations - maps from \parallel *C* Sigma
\parallel to (families of) sets of terms in \parallel \cal F
\parallel, where *C* Sigma is the syntactic category
constructed out of the lambda Pi-calculus with signature Sigma, and
\cal F is the category of families of sets. This construction is
similar to one of Miller, and exploits a Kripke-like satisfaction
predicate. We characterize this construction in terms of the model
theory of the lambda Pi-calculus using the Yoneda functor.

**PhD thesis - price £10.00**

*LFCS report ECS-LFCS-90-125 (also published as
CST-69-90)*