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-rst applications of rules in an appropriate sequent calculus, preferably without the redundancies generated by permutation of rules. This paper addresses the issues of dening such sequent calculi for Pure Type Systems (PTS, which are based on 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 dened by a system of local rewrite rules as in cut-elimination, using explicit substitutions. This system satises 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...

• Type: Journal
• Year: 2010
• Where: CORR
• Authors: Stéphane Lengrand, Roy Dyckhoff, James McKinna
• Keywords: CORR 2010, Education, Proof Search, PTSC, Sequent Calculus