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
DOIs
Publication statusPublished - 2001 Dec

ASJC Scopus subject areas

  • Philosophy
  • Logic

Fingerprint Dive into the research topics of 'A new correctness criterion for the proof nets of non-commutative multiplicative linear logics'. Together they form a unique fingerprint.

  • Cite this