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
Link To Document