System NEL is undecidable

Lutz Straßburger

doi:10.1016/S1571-0661(04)80853-3

System NEL is undecidable

Lutz Straßburger

Technical University Dresden

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

Abstract

System NEL is a conservative extension of multiplicative exponential linear logic (extended by the rules mix and nullary mix) by a self-dual noncommutative connective called seq which has an intermediate position between the connectives par and times. In this paper, I will show that system NEL is undecidable by encoding two counter machines into NEL. Although the encoding is simple, the proof of the faithfulness is a little intricate because there is no sequent calculus and no phase semantics available for NEL.

Original language	English
Pages (from-to)	166-177
Number of pages	12
Journal	Electronic Notes in Theoretical Computer Science
Volume	84
DOIs	https://doi.org/10.1016/S1571-0661(04)80853-3
Publication status	Published - 1 Jan 2003
Externally published	Yes

Access to Document

10.1016/S1571-0661(04)80853-3

Cite this

@article{ee4b36a048024b65b002dc6a900b132c,

title = "System NEL is undecidable",

abstract = "System NEL is a conservative extension of multiplicative exponential linear logic (extended by the rules mix and nullary mix) by a self-dual noncommutative connective called seq which has an intermediate position between the connectives par and times. In this paper, I will show that system NEL is undecidable by encoding two counter machines into NEL. Although the encoding is simple, the proof of the faithfulness is a little intricate because there is no sequent calculus and no phase semantics available for NEL.",

author = "Lutz Stra{\ss}burger",

year = "2003",

month = jan,

day = "1",

doi = "10.1016/S1571-0661(04)80853-3",

language = "English",

volume = "84",

pages = "166--177",

journal = "Electronic Notes in Theoretical Computer Science",

issn = "1571-0661",

}

TY - JOUR

T1 - System NEL is undecidable

AU - Straßburger, Lutz

PY - 2003/1/1

Y1 - 2003/1/1

N2 - System NEL is a conservative extension of multiplicative exponential linear logic (extended by the rules mix and nullary mix) by a self-dual noncommutative connective called seq which has an intermediate position between the connectives par and times. In this paper, I will show that system NEL is undecidable by encoding two counter machines into NEL. Although the encoding is simple, the proof of the faithfulness is a little intricate because there is no sequent calculus and no phase semantics available for NEL.

AB - System NEL is a conservative extension of multiplicative exponential linear logic (extended by the rules mix and nullary mix) by a self-dual noncommutative connective called seq which has an intermediate position between the connectives par and times. In this paper, I will show that system NEL is undecidable by encoding two counter machines into NEL. Although the encoding is simple, the proof of the faithfulness is a little intricate because there is no sequent calculus and no phase semantics available for NEL.

UR - https://www.scopus.com/pages/publications/4243396833

U2 - 10.1016/S1571-0661(04)80853-3

DO - 10.1016/S1571-0661(04)80853-3

M3 - Article

AN - SCOPUS:4243396833

SN - 1571-0661

VL - 84

SP - 166

EP - 177

JO - Electronic Notes in Theoretical Computer Science

JF - Electronic Notes in Theoretical Computer Science

ER -

System NEL is undecidable

Abstract

Access to Document

Other files and links

Fingerprint

Cite this