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

Misao Nagayama, Mitsuhiro Okada

Research output: Contribution to journalConference article

1 Citation (Scopus)


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].

Original languageEnglish
Pages (from-to)551-573
Number of pages23
JournalTheoretical Computer Science
Issue number3
Publication statusPublished - 2003 Feb 18
Externally publishedYes
EventLinear Logic - Tokyo, Japan
Duration: 1996 Mar 281996 Apr 2



  • Linear logic
  • Non-commutative logic
  • Planar graph
  • Proof net
  • Sequentialization theorem

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

Cite this