A Non-commutative Extension of Multiplicative Exponential Linear Logic

摘要: We extend multiplicative exponential linear logic (MELL) by a non- commutative, self-dual logical operator. The extended system, called NEL, is defined in the formalism of calculus structures, which generalisation sequent and provides more refined analysis proofs. are then able to expressiveness MELL modelling broad notion sequentiality. show some proof theoretical results: decomposition cut elimination. new operator represents significant challenge: get our results we use here for first time novel techniques, constitute uniform modular approach elimination, contrary what possible calculus.