A Focused Sequent Calculus Framework for Proof Search in Pure Type Systems
Résumé
Basic proof search tactics in logic and type theory can be seen as the root-rst applications of rules in an appropriate sequent calculus, preferably without the redundancies generated by permutation of rules. This paper ad-dresses the issues of dening such sequent calculi for Pure Type Systems (PTS, which are based on natural deduction) and then organizing their rules for ef-fective proof search. First, we introduce the idea of a Pure Type Sequent Calculus (PTSC) by enriching a permutation-free sequent calculus for propo-sitional 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 dened by a system of local rewrite rules as in cut-elimination, using explicit substitutions. This system satis-es the Subject Reduction property and is conuent. Each PTSC is logically equivalent to its corresponding PTS, and the former is strongly normalising i 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 ex-tension PTSCα 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 unication.
Origine : Fichiers produits par l'(les) auteur(s)
Loading...
