Article ID | Journal | Published Year | Pages | File Type |
---|---|---|---|---|
10118867 | Annals of Pure and Applied Logic | 2005 | 48 Pages |
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 LKpolη and LKpolη,Ï perfectly fits normalization of polarized proof-nets. Some more semantical considerations allow us to recover LC as a refinement of multiplicative LKpolη.
Keywords
Related Topics
Physical Sciences and Engineering
Mathematics
Logic
Authors
Olivier Laurent, Myriam Quatrini, Lorenzo Tortora de Falco,