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.
|Number of pages||19|
|Journal||Journal of Symbolic Logic|
|Publication status||Published - 2001 Dec|
ASJC Scopus subject areas