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