MR1489405 (98m:03120) In sequent calculus, MIX refers to the following structural rule: From Gamma => Delta and Pi => \Lambda infer \Gamma, Pi => Delta\Lambda. On top of classical linear logic, MIX is equivalent to assuming the axiom bot => 1. Thus it is validated in current denotational semantics in coherence spaces. From the viewpoint of proof-nets, MIX leaves room for disconnected graphs. The paper focuses on the system ${\rm MLL-+ MIX (which we call here LB), where MLL-} is first-order multiplicative linear logic without constants. The first section of the paper is an overview of results involving the rule MIX in various settings. The main results are: (1) a new proof of sequentialization for LB, whose distinctive feature is a direct use of the ordering of kingdoms, without reducing the problem to that for MLL; (2) the extension of the criterion for proof-nets for the propositional part of LB from a paper by A. Asperti [Math. Structures Comput. Sci. 5 (1995), no. 3, 351--380, MR1361605 (96g:03098)]to the first-order case. There is also a proof of sequentialization for the system FILL + MIX, where FILL is the system of J. M. E. Hyland and V. C. V. de Paiva [Ann. Pure Appl. Logic 64 (1993), no. 3, 273--291 MR1253832 ], which uses an "input-output orientation" of proof-nets. (Reviewed by Aldo Ursini) Recent citations: O Kahramanogulları System BV is NP-complete Electronic Notes in Theoretical Computer Science Volume 143, 6, 2006, pp. 87-99 Proceedings of WoLLIC 2005 T Brauner. A cut-free Gentzen formulation of the modal logic S5 Logic Journal of IGPL, 2000 - Oxford Univ Press L. Caires, L. Monteiro. Proof Net Semantics of Proof Search Computation Proceedings of the 6th International Joint Conference on Algebraic and Logic Programming, Lecture Notes In Computer Science; Vol. 1298, 1997, pp. 194 - 208

Subnets of Proof-nets in multiplicative linear logic with MIX

BELLIN, Gianluigi
1997-01-01

Abstract

MR1489405 (98m:03120) In sequent calculus, MIX refers to the following structural rule: From Gamma => Delta and Pi => \Lambda infer \Gamma, Pi => Delta\Lambda. On top of classical linear logic, MIX is equivalent to assuming the axiom bot => 1. Thus it is validated in current denotational semantics in coherence spaces. From the viewpoint of proof-nets, MIX leaves room for disconnected graphs. The paper focuses on the system ${\rm MLL-+ MIX (which we call here LB), where MLL-} is first-order multiplicative linear logic without constants. The first section of the paper is an overview of results involving the rule MIX in various settings. The main results are: (1) a new proof of sequentialization for LB, whose distinctive feature is a direct use of the ordering of kingdoms, without reducing the problem to that for MLL; (2) the extension of the criterion for proof-nets for the propositional part of LB from a paper by A. Asperti [Math. Structures Comput. Sci. 5 (1995), no. 3, 351--380, MR1361605 (96g:03098)]to the first-order case. There is also a proof of sequentialization for the system FILL + MIX, where FILL is the system of J. M. E. Hyland and V. C. V. de Paiva [Ann. Pure Appl. Logic 64 (1993), no. 3, 273--291 MR1253832 ], which uses an "input-output orientation" of proof-nets. (Reviewed by Aldo Ursini) Recent citations: O Kahramanogulları System BV is NP-complete Electronic Notes in Theoretical Computer Science Volume 143, 6, 2006, pp. 87-99 Proceedings of WoLLIC 2005 T Brauner. A cut-free Gentzen formulation of the modal logic S5 Logic Journal of IGPL, 2000 - Oxford Univ Press L. Caires, L. Monteiro. Proof Net Semantics of Proof Search Computation Proceedings of the 6th International Joint Conference on Algebraic and Logic Programming, Lecture Notes In Computer Science; Vol. 1298, 1997, pp. 194 - 208
1997
Mix rule; subnets of proof-nets; Multiplicative Linear Logic; correctness; concurrent processes; sequentialization.
File in questo prodotto:
File Dimensione Formato  
BellinMSCS1997.pdf

accesso aperto

Tipologia: Documento in Pre-print
Licenza: Dominio pubblico
Dimensione 1.07 MB
Formato Adobe PDF
1.07 MB Adobe PDF Visualizza/Apri

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/11562/30363
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus ND
  • ???jsp.display-item.citation.isi??? ND
social impact