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

Misao Nagayama, Mitsuhiro Okada

Research output: Contribution to journalArticle

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 languageEnglish
Pages (from-to)1524-1542
Number of pages19
JournalJournal of Symbolic Logic
Volume66
Issue number4
Publication statusPublished - 2001 Dec

Fingerprint

Proof Nets
Linear Logic
Correctness
Multiplicative
Graph in graph theory
Research and Development
Linear Time
Corollary
Graph

ASJC Scopus subject areas

  • Logic

Cite this

A new correctness criterion for the proof nets of non-commutative multiplicative linear logics. / Nagayama, Misao; Okada, Mitsuhiro.

In: Journal of Symbolic Logic, Vol. 66, No. 4, 12.2001, p. 1524-1542.

Research output: Contribution to journalArticle

@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 = "12",
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

M3 - Article

AN - SCOPUS:0035732340

VL - 66

SP - 1524

EP - 1542

JO - Journal of Symbolic Logic

JF - Journal of Symbolic Logic

SN - 0022-4812

IS - 4

ER -