• Title of article

    Polarized and focalized linear and classical proofs

  • Author/Authors

    Laurent، نويسنده , , Olivier and Quatrini، نويسنده , , Myriam and Tortora de Falco، نويسنده , , Lorenzo، نويسنده ,

  • Issue Information
    روزنامه با شماره پیاپی سال 2005
  • Pages
    48
  • From page
    217
  • To page
    264
  • Abstract
    We give the precise correspondence between polarized linear logic and polarized classical logic. The properties of focalization and reversion of linear proofs are at the heart of our analysis: we show that the tq-protocol of normalization for the classical systems LK pol η and LK pol η , ρ perfectly fits normalization of polarized proof-nets. Some more semantical considerations allow us to recover LC as a refinement of multiplicative LK pol η .
  • Keywords
    Proof-nets , Denotational semantics , Polarization , focalization , reversion , Classical logic , Linear logic , cut-elimination
  • Journal title
    Annals of Pure and Applied Logic
  • Serial Year
    2005
  • Journal title
    Annals of Pure and Applied Logic
  • Record number

    1443652