TY - JOUR

T1 - A graph-theoretic characterization theorem for multiplicative fragment of non-commutative linear logic

AU - Nagayama, Misao

AU - Okada, Mitsuhiro

PY - 2003/2/18

Y1 - 2003/2/18

N2 - It is well known that every proof net of a non-commutative version of MLL (multiplicative fragment of commutative linear logic) can be drawn as a plane Danos-Regnier graph (drawing) satisfying the switching condition of Danos-Regnier [3]. In this paper, we study the reverse direction; we introduce a system MNCLL which is logically equivalent to the multiplicative fragment of cyclic linear logic introduced by Yetter [9], and show that any plane Danos-Regnier graph drawing with one terminal edge satisfying the switching condition represents a unique non-commutative proof net (i.e., a proof net of MNCLL). In the course of proving this, we also give the characterization of the non-commutative proof nets by means of the notion of strong planarity, as well as the notion of a certain long-trip condition, called the stack-condition, of a Danos-Regnier graph, the latter of which is related to Abrusci's balanced long-trip condition [2].

AB - It is well known that every proof net of a non-commutative version of MLL (multiplicative fragment of commutative linear logic) can be drawn as a plane Danos-Regnier graph (drawing) satisfying the switching condition of Danos-Regnier [3]. In this paper, we study the reverse direction; we introduce a system MNCLL which is logically equivalent to the multiplicative fragment of cyclic linear logic introduced by Yetter [9], and show that any plane Danos-Regnier graph drawing with one terminal edge satisfying the switching condition represents a unique non-commutative proof net (i.e., a proof net of MNCLL). In the course of proving this, we also give the characterization of the non-commutative proof nets by means of the notion of strong planarity, as well as the notion of a certain long-trip condition, called the stack-condition, of a Danos-Regnier graph, the latter of which is related to Abrusci's balanced long-trip condition [2].

KW - Linear logic

KW - Non-commutative logic

KW - Planar graph

KW - Proof net

KW - Sequentialization theorem

UR - http://www.scopus.com/inward/record.url?scp=0037452396&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=0037452396&partnerID=8YFLogxK

U2 - 10.1016/S0304-3975(01)00178-5

DO - 10.1016/S0304-3975(01)00178-5

M3 - Conference article

AN - SCOPUS:0037452396

VL - 294

SP - 551

EP - 573

JO - Theoretical Computer Science

JF - Theoretical Computer Science

SN - 0304-3975

IS - 3

T2 - Linear Logic

Y2 - 28 March 1996 through 2 April 1996

ER -