MR1634276 (99m:03120) The authors consider representations of proofs as graphs for the multiplicative fragment of linear logic with the mix-rule in the planar and braided cases. They give two interesting characterizations of planar representations of proofs, one representing proof-nets as CW-complexes in a two-dimensional disc, the other extending Asperti's characterization of proofs as concurrent processes. In order to prove the cut-elimination theorem, the authors consider planar proof-nets as projections of three-dimensional objects, braided proof-nets under regular isotopy. (Reviewed by R. Gylys) Cited by: Métayer, F. Implicit exchange in multiplicative proofnets. Math. Struct. Comput. Sci. 11, No.2, 261-272 (2001). Gaubert, C.Two-dimensional proof-structures and the exchange rule. [Math. Struct. Comput. Sci. 14, No. 1, 73-96 (2004) Andreoli J-M; Pulcini G. ; Ruet P. Permutative logic: a geometrical study on linear logic proofs, Computer Science Logic. Springer. LNCS 3634: 184-199, 2005 G.Pulcini. Permutative Additives and Exponentials, In: Logic for Programming, Artificial Intelligence, and Reasoning, Springer Lecture Notes in Computer Science Vol. 4790, 2007

Planar and Braided Proof-nets for MLL with Mix

BELLIN, Gianluigi;FLEURY, Arnaud
1998-01-01

Abstract

MR1634276 (99m:03120) The authors consider representations of proofs as graphs for the multiplicative fragment of linear logic with the mix-rule in the planar and braided cases. They give two interesting characterizations of planar representations of proofs, one representing proof-nets as CW-complexes in a two-dimensional disc, the other extending Asperti's characterization of proofs as concurrent processes. In order to prove the cut-elimination theorem, the authors consider planar proof-nets as projections of three-dimensional objects, braided proof-nets under regular isotopy. (Reviewed by R. Gylys) Cited by: Métayer, F. Implicit exchange in multiplicative proofnets. Math. Struct. Comput. Sci. 11, No.2, 261-272 (2001). Gaubert, C.Two-dimensional proof-structures and the exchange rule. [Math. Struct. Comput. Sci. 14, No. 1, 73-96 (2004) Andreoli J-M; Pulcini G. ; Ruet P. Permutative logic: a geometrical study on linear logic proofs, Computer Science Logic. Springer. LNCS 3634: 184-199, 2005 G.Pulcini. Permutative Additives and Exponentials, In: Logic for Programming, Artificial Intelligence, and Reasoning, Springer Lecture Notes in Computer Science Vol. 4790, 2007
1998
Planar proof-nets; projections under regular isotopy; braided proof-nets; noncommutative proof-nets; explicit exchange rule; CW-complexes; correctness; planar graphs; multiplicative linear logic with Mix; cut-elimination theorem.
File in questo prodotto:
File Dimensione Formato  
art%3A10.1007%2Fs001530050101.pdf

accesso aperto

Tipologia: Documento in Post-print
Licenza: Dominio pubblico
Dimensione 566.82 kB
Formato Adobe PDF
566.82 kB 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/30362
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus ND
  • ???jsp.display-item.citation.isi??? ND
social impact