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 (defined by Danos, Joinet and Schellinx for the classical systems LKeta and polarized LKeta perfectly fits normalization of polarized proof-nets. In the last section, some more semantical considerations allow to recover LC as a refinement of multiplicative polarized LKeta.
Laurent, O., Quatrini, M., TORTORA DE FALCO, L. (2005). Polarized and focalized linear and classical proofs. ANNALS OF PURE AND APPLIED LOGIC, 134 (2-3), 217-263.
Polarized and focalized linear and classical proofs
TORTORA DE FALCO, LORENZO
2005-01-01
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 (defined by Danos, Joinet and Schellinx for the classical systems LKeta and polarized LKeta perfectly fits normalization of polarized proof-nets. In the last section, some more semantical considerations allow to recover LC as a refinement of multiplicative polarized LKeta.I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.