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 -