## Proof Search in the lambda-Pi-calculus

**David Pym and Lincoln Wallen**
*Abstract:* We formulate a system for proof-search in the
lambda-Pi-calculus by exploiting a cut-elimination theorem and a
subformula property. We modify this system to support the use of
unification and prove that the modification reduces the search
space uniformly. A permutation theorem is then exploited to reduce
the search space further and a notion of *intrinsic
well-typing* is introduced to ensure an adequate computational
basis for proof-search.

*LFCS report ECS-LFCS-91-146*

Previous |

Index |

Next