TY - GEN
T1 - A non-commutative extension of MELL
AU - Guglielmi, Alessio
AU - Straßburger, Lutz
N1 - Publisher Copyright:
© Springer-Verlag Berlin Heidelberg 2002.
PY - 2002/1/1
Y1 - 2002/1/1
N2 - We extend multiplicative exponential linear logic (M E L) L by a non-commutative, self-dual logical operator.The extended system, called N EL, 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 should then be able to extend the range of applications of M E L,L by modelling a broad notion of sequentiality and providing new properties of proofs. 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 the sequent calculus.
AB - We extend multiplicative exponential linear logic (M E L) L by a non-commutative, self-dual logical operator.The extended system, called N EL, 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 should then be able to extend the range of applications of M E L,L by modelling a broad notion of sequentiality and providing new properties of proofs. 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 the sequent calculus.
U2 - 10.1007/3-540-36078-6_16
DO - 10.1007/3-540-36078-6_16
M3 - Conference contribution
AN - SCOPUS:84954456619
SN - 3540000100
SN - 9783540000105
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 231
EP - 246
BT - Logic for Programming, Artificial Intelligence, and Reasoning - 9th International Conference, LPAR 2002, Proceedings
A2 - Baaz, Matthias
A2 - Voronkov, Andrei
PB - Springer Verlag
T2 - 9th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning, LPAR 2002
Y2 - 14 October 2002 through 18 October 2002
ER -