A Focused Sequent Calculus Framework for

Niveau: Supérieur
A Focused Sequent Calculus Framework for Proof Search in Pure Type Systems Stéphane Lengrand 1 , Roy Dyckho? 2 and James McKinna 3 1 CNRS, École Polytechnique, France. 2 School of Computer Science, University of St Andrews, Scotland. 3 Radboud University, Nijmegen, The Netherlands. 3rd October 2009 Abstract 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 ad- dresses the issues of defining 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 defined by a system of local rewrite rules as in cut-elimination, using explicit substitutions. This system satis- fies the Subject Reduction property and is confluent.

• inference rules


• using meta-variables


• can also


• system pe


• pts g3 ?


• defining such


• proof construction


• typing system