Article ID Journal Published Year Pages File Type
10118867 Annals of Pure and Applied Logic 2005 48 Pages PDF
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η.
Related Topics
Physical Sciences and Engineering Mathematics Logic
Authors
, , ,