## 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 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 language | English |
---|---|

Pages (from-to) | 551-573 |

Number of pages | 23 |

Journal | Theoretical Computer Science |

Volume | 294 |

Issue number | 3 |

DOIs | |

Publication status | Published - 2003 Feb 18 |

Event | Linear Logic - Tokyo, Japan Duration: 1996 Mar 28 → 1996 Apr 2 |

## Keywords

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

## ASJC Scopus subject areas

- Theoretical Computer Science
- Computer Science(all)