A graph-theoretic characterization theorem for multiplicative fragment of non-commutative linear logic
| Autor: | Misao Nagayama, Mitsuhiro Okada |
|---|---|
| Rok vydání: | 2003 |
| Předmět: |
Discrete mathematics
General Computer Science Graph theoretic Logical equivalence Multiplicative function Linear logic Sequentialization theorem Planarity testing Theoretical Computer Science Planar graph Combinatorics Graph drawing Computer Science::Logic in Computer Science Non-commutative logic Proof net Commutative property Computer Science(all) Mathematics |
| Zdroj: | Theoretical Computer Science. 294:551-573 |
| ISSN: | 0304-3975 |
| DOI: | 10.1016/s0304-3975(01)00178-5 |
| 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 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]. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|
Full Text from ScienceDirect