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.
2005
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.
File in questo prodotto:
Non ci sono file associati a questo prodotto.

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/11590/143361
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 15
  • ???jsp.display-item.citation.isi??? 14
social impact