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
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
Journal title :
Annals of Pure and Applied Logic