A Graph-Theoretic Characterization Theorem for Multiplicative Fragment of Non-Commutative Linear Logic (Extended Abstract)

Misao Nagayama, Mitsuhiro Okada

Research output: Contribution to journalArticle

6 Citations (Scopus)

Abstract

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 logically equivalent to the multiplicative fragment of Cyclic Linear Logic introduced by Yetter [9], and show that any plane Danos-Regnier graph drawing satisfying the switching condition represents a unique non-commutative proof net (i.e., a proof net of MNCLL) modulo cyclic shifts. In the course of proving this, we also give the characterization of the non-commutative proof nets by means of the notion of strong planity, 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 balanced long-trip condition [2].

Original languageEnglish
Pages (from-to)153
Number of pages1
JournalElectronic Notes in Theoretical Computer Science
Volume3
Issue numberC
DOIs
Publication statusPublished - 1996

Fingerprint

Linear Logic
Characterization Theorem
Proof Nets
Multiplicative
Fragment
Graph in graph theory
Graph Drawing
Tautologous
Modulo
Reverse

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)
  • Computer Science (miscellaneous)

Cite this

@article{e3adc4c55ea94215bee2adb884fcf2f7,
title = "A Graph-Theoretic Characterization Theorem for Multiplicative Fragment of Non-Commutative Linear Logic (Extended Abstract)",
abstract = "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 logically equivalent to the multiplicative fragment of Cyclic Linear Logic introduced by Yetter [9], and show that any plane Danos-Regnier graph drawing satisfying the switching condition represents a unique non-commutative proof net (i.e., a proof net of MNCLL) modulo cyclic shifts. In the course of proving this, we also give the characterization of the non-commutative proof nets by means of the notion of strong planity, 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 balanced long-trip condition [2].",
author = "Misao Nagayama and Mitsuhiro Okada",
year = "1996",
doi = "10.1016/S1571-0661(05)82518-6",
language = "English",
volume = "3",
pages = "153",
journal = "Electronic Notes in Theoretical Computer Science",
issn = "1571-0661",
publisher = "Elsevier",
number = "C",

}

TY - JOUR

T1 - A Graph-Theoretic Characterization Theorem for Multiplicative Fragment of Non-Commutative Linear Logic (Extended Abstract)

AU - Nagayama, Misao

AU - Okada, Mitsuhiro

PY - 1996

Y1 - 1996

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 logically equivalent to the multiplicative fragment of Cyclic Linear Logic introduced by Yetter [9], and show that any plane Danos-Regnier graph drawing satisfying the switching condition represents a unique non-commutative proof net (i.e., a proof net of MNCLL) modulo cyclic shifts. In the course of proving this, we also give the characterization of the non-commutative proof nets by means of the notion of strong planity, 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 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 logically equivalent to the multiplicative fragment of Cyclic Linear Logic introduced by Yetter [9], and show that any plane Danos-Regnier graph drawing satisfying the switching condition represents a unique non-commutative proof net (i.e., a proof net of MNCLL) modulo cyclic shifts. In the course of proving this, we also give the characterization of the non-commutative proof nets by means of the notion of strong planity, 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 balanced long-trip condition [2].

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

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

U2 - 10.1016/S1571-0661(05)82518-6

DO - 10.1016/S1571-0661(05)82518-6

M3 - Article

VL - 3

SP - 153

JO - Electronic Notes in Theoretical Computer Science

JF - Electronic Notes in Theoretical Computer Science

SN - 1571-0661

IS - C

ER -