A Non-commutative Extension of Multiplicative Exponential Linear Logic

Alessio Guglielmi, L Straßburger

Research output: Working paperDiscussion paper

Abstract

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

Fingerprint

Cut-elimination
Linear Logic
Multiplicative
Logical operator
Sequent Calculus
Extended Systems
Expressiveness
Calculus
Decompose
Operator
Modeling
Generalization

Cite this

Guglielmi, A., & Straßburger, L. (2004). A Non-commutative Extension of Multiplicative Exponential Linear Logic. Technische Universitaet Dresden.

A Non-commutative Extension of Multiplicative Exponential Linear Logic. / Guglielmi, Alessio; Straßburger, L.

Technische Universitaet Dresden, 2004.

Research output: Working paperDiscussion paper

Guglielmi, A & Straßburger, L 2004 'A Non-commutative Extension of Multiplicative Exponential Linear Logic' Technische Universitaet Dresden.
Guglielmi A, Straßburger L. A Non-commutative Extension of Multiplicative Exponential Linear Logic. Technische Universitaet Dresden. 2004.
Guglielmi, Alessio ; Straßburger, L. / A Non-commutative Extension of Multiplicative Exponential Linear Logic. Technische Universitaet Dresden, 2004.
@techreport{27d7a371250f4674bb6c589b37642d9f,
title = "A Non-commutative Extension of Multiplicative Exponential Linear Logic",
abstract = "We extend multiplicative exponential linear logic (MELL) by a noncommutative, self-dual logical operator. The extended system, called NEL, is defined in the formalism of the calculus of structures, which is a generalisation of the sequent calculus and provides a more refined analysis of proofs. We are then able to extend the expressiveness of MELL by modelling a broad notion of sequentiality. We show some proof theoretical results: decomposition and cut elimination. The new operator represents a significant challenge: to get our results we use here for the first time some novel techniques, which constitute a uniform and modular approach to cut elimination, contrary to what is possible in",
author = "Alessio Guglielmi and L Stra{\ss}burger",
year = "2004",
language = "English",
type = "WorkingPaper",

}

TY - UNPB

T1 - A Non-commutative Extension of Multiplicative Exponential Linear Logic

AU - Guglielmi, Alessio

AU - Straßburger, L

PY - 2004

Y1 - 2004

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

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

UR - http://www.ps.uni-sb.de/~lutz/papers/NELbig.pdf

M3 - Discussion paper

BT - A Non-commutative Extension of Multiplicative Exponential Linear Logic

CY - Technische Universitaet Dresden

ER -