A Graph-Theoretic Characterization Theorem for Multiplicative Fragment of Non-Commutative Linear Logic (Extended Abstract)
| Autor: | Mitsuhiro Okada, Misao Nagayama |
|---|---|
| Jazyk: | angličtina |
| Předmět: |
Discrete mathematics
General Computer Science Multiplicative function Linear logic Theoretical Computer Science Combinatorics Fragment (logic) Graph drawing Computer Science::Logic in Computer Science Graph (abstract data type) Structural proof theory Proof net Commutative property Computer Science(all) Mathematics |
| Zdroj: | Electronic Notes in Theoretical Computer Science. :153 |
| ISSN: | 1571-0661 |
| DOI: | 10.1016/S1571-0661(05)82518-6 |
| Popis: | 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]. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|