A Focused Sequent Calculus Framework for Proof Search in Pure Type Systems

Basic proof search tactics in logic and type theory can be seen as the root-first applications of rules in an appropriate sequent calculus, preferably without the redundancies generated by permutation of rules. This paper addresses the issues of defining such sequent calculi for Pure Type Systems (PTS, which were originally presented in natural deduction) and then organizing their rules for effective proof search. First, we introduce the idea of a Pure Type Sequent Calculus (PTSC) by enriching a permutation-free sequent calculus for propositional logic due to Herbelin, which is strongly related to natural deduction and already well adapted to proof-search. Such a PTSC admits a normalisation procedure, adapted from Herbelin's and defined by a system of local rewrite rules as in cut-elimination, using explicit substitutions. This system satisfies the Subject Reduction property and is confluent. Each PTSC is logically equivalent to its corresponding PTS, and the former is strongly normalising iff the latter is. Second, we make the logical rules of PTSC syntax-directed for proof search, by incorporating the conversion rules as in syntax-directed presentations of the PTS rules for type checking. Third, we consider an extension PTSCa of PTSC with explicitly scoped meta-variables, representing partial proof-terms, and use it to analyse interactive proof construction. This sets up a framework in which we are able to study proof-search strategies, type inhabitant enumeration and unification.