## Investigations into proof-search in a system of first-order
dependent function types

**David Pym and Lincoln Wallen**
*Abstract:* We present a series of proof systems for lambda
Pi-calculus: a theory of *first-order dependent function
types*. The systems are complete for the judgement of interest
but differ substantially as bases for algorithmic proof-search.
Each calculus in the series induces a search space that is properly
contained within that of its predecessor. The lambda Pi-calculus is
a candidate *general logic* in that it provides a metalanguage
suitable for the encoding of logical systems and mathematics. Proof
procedures formulated for the metalanguage extend to suitably
encoded object logics, thus removing the need to develop procedures
for each logic independently. This work is also an exploration of a
*systematic* approach to the design of proof procedures. It is
our contention that the task of designing a computationally
efficient proof procedure for a given logic can be approached by
formulating a series of calculi that possess specific
proof-theoretic properties. These properties indicate that standard
computational techniques such as *unification* are applicable,
sometimes in novel ways. The study below is an application of this
design method to an intuitionistic type theory.

Our methods exploit certain forms of *subformula property*
and *reduction ordering* - a notion introduced by Bibel for
classical logic, and extended by Wallen to various non-classical
logics - to obtain a search calculus for which we are able to
define notions of *computability* and *intrinsic
well-typing* between a derivation psi and a substitution sigma
calculated by unification which closes psi (a derivation is closed
when all of its leaves are axioms). Compatibility is an acyclicity
test, a generalization of the *occurs-check* which, subject to
intrinsic well-typing, determines whether the derivation psi and
substitution sigma together constitute a *proof*

Our work yields the (operational) foundations for a study of
*logic programming* in this general setting. This potential is
not explored here.

*LFCS report ECS-LFCS-90-111*

Previous |

Index |

Next