Proofs, search and computation in general logic
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 λII-calculus, the λ-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 λII- 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 λII- calculus is decidable. We present a theory of search and logic programming for the λII- calculus and consequently for logics which are adequately represented in the LF. The presentation of the .AH-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 II-elimination rule is replaced by a sequent calculus style II-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 λII- calculus which forms a suitable basis for proof-search in the λII-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 λII- calculus by extending the work of Huet for the simply-typed A-calculus. We use this unification algorithm to allow us to eliminate non-deterministic choices of terms, when performing proof-search with the (lll) 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 firstorder classical, modal and intuitionistic logics) to the λII- 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 |C(E∑)| to (families of) sets of terms in |F|, where C(∑) is the syntactic category constructed out of the λII -calculus with signature ∑, and 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 All-calculus using the Yoneda functor.