A new correctness criterion for the proof nets of non-commutative multiplicative linear logics

Misao Nagayama; Mitsuhiro Okada

doi:10.2307/2694960

A new correctness criterion for the proof nets of non-commutative multiplicative linear logics

Misao Nagayama, Mitsuhiro Okada

Department of Philosophy

Research output: Contribution to journal › Article › peer-review

1 Citation (Scopus)

Abstract

This paper presents a new correctness criterion for marked Danos-Reginer graphs ( D-R graphs, for short) of Multiplicative Cyclic Linear Logic MCLL and Abrusci's non-commutative Linear Logic MNLL. As a corollary we obtain an affirmative answer to the open question whether a known quadratic-time algorithm for the correctness checking of proof nets for MCLL and MNLL can be improved to linear-time.

Original language	English
Pages (from-to)	1524-1542
Number of pages	19
Journal	Journal of Symbolic Logic
Volume	66
Issue number	4
DOIs	https://doi.org/10.2307/2694960
Publication status	Published - 2001 Dec

ASJC Scopus subject areas

Philosophy
Logic

Access to Document

10.2307/2694960

Cite this

@article{57efd0f2fe264611981ceb325e34cd51,

title = "A new correctness criterion for the proof nets of non-commutative multiplicative linear logics",

abstract = "This paper presents a new correctness criterion for marked Danos-Reginer graphs ( D-R graphs, for short) of Multiplicative Cyclic Linear Logic MCLL and Abrusci's non-commutative Linear Logic MNLL. As a corollary we obtain an affirmative answer to the open question whether a known quadratic-time algorithm for the correctness checking of proof nets for MCLL and MNLL can be improved to linear-time.",

author = "Misao Nagayama and Mitsuhiro Okada",

year = "2001",

month = dec,

doi = "10.2307/2694960",

language = "English",

volume = "66",

pages = "1524--1542",

journal = "Journal of Symbolic Logic",

issn = "0022-4812",

publisher = "Association for Symbolic Logic",

number = "4",

}

TY - JOUR

T1 - A new correctness criterion for the proof nets of non-commutative multiplicative linear logics

AU - Nagayama, Misao

AU - Okada, Mitsuhiro

PY - 2001/12

Y1 - 2001/12

N2 - This paper presents a new correctness criterion for marked Danos-Reginer graphs ( D-R graphs, for short) of Multiplicative Cyclic Linear Logic MCLL and Abrusci's non-commutative Linear Logic MNLL. As a corollary we obtain an affirmative answer to the open question whether a known quadratic-time algorithm for the correctness checking of proof nets for MCLL and MNLL can be improved to linear-time.

AB - This paper presents a new correctness criterion for marked Danos-Reginer graphs ( D-R graphs, for short) of Multiplicative Cyclic Linear Logic MCLL and Abrusci's non-commutative Linear Logic MNLL. As a corollary we obtain an affirmative answer to the open question whether a known quadratic-time algorithm for the correctness checking of proof nets for MCLL and MNLL can be improved to linear-time.

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

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

U2 - 10.2307/2694960

DO - 10.2307/2694960

M3 - Article

AN - SCOPUS:0035732340

SN - 0022-4812

VL - 66

SP - 1524

EP - 1542

JO - Journal of Symbolic Logic

JF - Journal of Symbolic Logic

IS - 4

ER -

A new correctness criterion for the proof nets of non-commutative multiplicative linear logics

Abstract

ASJC Scopus subject areas

Access to Document

Other files and links

Fingerprint

Cite this