Canonical Sequent Proofs via Multi Focusing

icon

15

pages

icon

English

icon

Documents

Écrit par

Publié par

Lire un extrait
Lire un extrait

Obtenez un accès à la bibliothèque pour le consulter en ligne En savoir plus

Découvre YouScribe en t'inscrivant gratuitement

Je m'inscris

Découvre YouScribe en t'inscrivant gratuitement

Je m'inscris
icon

15

pages

icon

English

icon

Ebook

Lire un extrait
Lire un extrait

Obtenez un accès à la bibliothèque pour le consulter en ligne En savoir plus

Niveau: Supérieur
Canonical Sequent Proofs via Multi-Focusing Kaustuv Chaudhuri, Dale Miller, and Alexis Saurin Abstract The sequent calculus admits many proofs of the same conclusion that differ only by trivial permutations of inference rules. In order to eliminate this “bu- reaucracy” from sequent proofs, deductive formalisms such as proof nets or natural deduction are usually used instead of the sequent calculus, for they identify proofs more abstractly and geometrically. In this paper we recover permutative canonicity directly in the cut-free sequent calculus by generalizing focused sequent proofs to admit multiple foci, and then considering the restricted class of maximally multi- focused proofs. We validate this definition by proving a bijection to the well-known proof-nets for the unit-free multiplicative linear logic, and discuss the possibility of a similar correspondence for larger fragments. 1 Introduction Sequent calculus proofs are much less proof objects than they are traces of the com- putation of a more abstract proof object. In particular, the infernece rules of the sequent calculus are minute and there are many choices in the order of their applica- tion that seem equivalent although, formally, they result in different sequent proofs. One way to get a more abstract notion of proof is to declare that two cut-free proofs are equivalent if it is possible to permute the inference rules in one to get the other. Such equivalence classes are unsatisfactory for at least two reasons.

  • inference rules

  • consider only

  • multi-focused proofs

  • when deciding

  • rule

  • problematic when

  • local permutation

  • rules


Voir Alternate Text

Publié par

Nombre de lectures

13

Langue

English

CanonicalSequentProofsviaMulti-FocusingKaustuvChaudhuri,DaleMiller,andAlexisSaurinAbstractThesequentcalculusadmitsmanyproofsofthesameconclusionthatdieronlybytrivialpermutationsofinferencerules.Inordertoeliminatethis“bu-reaucracy”fromsequentproofs,deductiveformalismssuchasproofnetsornaturaldeductionareusuallyusedinsteadofthesequentcalculus,fortheyidentifyproofsmoreabstractlyandgeometrically.Inthispaperwerecoverpermutativecanonicitydirectlyinthecut-freesequentcalculusbygeneralizingfocusedsequentproofstoadmitmultiplefoci,andthenconsideringtherestrictedclassofmaximallymulti-focusedproofs.Wevalidatethisdenitionbyprovingabijectiontothewel-knownproof-netsfortheunit-freemultiplicativelinearlogic,anddiscussthepossibilityofasimilarcorrespondenceforlargerfragments.1IntroductionSequentcalculusproofsaremuchlessproofobjectsthantheyaretracesofthecom-putationofamoreabstractproofobject.Inparticular,theinfernecerulesofthesequentcalculusareminuteandtherearemanychoicesintheorderoftheirapplica-tionthatseemequivalentalthough,formally,theyresultindierentsequentproofs.Onewaytogetamoreabstractnotionofproofistodeclarethattwocut-freeproofsareequivalentifitispossibletopermutetheinferencerulesinonetogettheother.Suchequivalenceclassesareunsatisfactoryforatleasttworeasons.First,com-putingpermutationsofinferencerulesmightrequireexaminingandreorganizingKaustuvChaudhuriINRIASaclay–Iˆle-de-France,e-mail:Kaustuv.Chaudhuri@inria.frDaleMillerINRIASaclay–Iˆle-de-France&LIX,E´colePolytechnique,e-mail:Dale.Miller@inria.frAlexisSaurinINRIASaclay–Iˆle-de-France&LIX,E´colePolytechnique,e-mail:Alexis.Saurin@inria.fr1
Voir Alternate Text
  • Univers Univers
  • Ebooks Ebooks
  • Livres audio Livres audio
  • Presse Presse
  • Podcasts Podcasts
  • BD BD
  • Documents Documents
Alternate Text