Sciweavers

Share
CORR
2010
Springer

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

8 years 2 months ago
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...
Stéphane Lengrand, Roy Dyckhoff, James McKi
Added 01 Mar 2011
Updated 01 Mar 2011
Type Journal
Year 2010
Where CORR
Authors Stéphane Lengrand, Roy Dyckhoff, James McKinna
Comments (0)
books