TY - JOUR
T1 - A system of interaction and structure V: the exponentials and splitting
AU - Guglielmi, Alessio
AU - Straburger, L
PY - 2011/6
Y1 - 2011/6
N2 - System NEL is the mixed commutative/non-commutative linear logic BV augmented with linear logic's exponentials, or, equivalently, it is MELL augmented with the non-commutative self-dual connective seq. NEL is presented in deep inference, because no Gentzen formalism can express it in such a way that the cut rule is admissible. Other recent work shows that system NEL is Turing-complete, and is able to express process algebra sequential composition directly and model causal quantum evolution faithfully. In this paper, we show cut elimination for NEL, based on a technique that we call splitting. The splitting theorem shows how and to what extent we can recover a sequent-like structure in NEL proofs. When combined with a 'decomposition' theorem, proved in the previous paper of this series, splitting yields a cut-elimination procedure for NEL.
AB - System NEL is the mixed commutative/non-commutative linear logic BV augmented with linear logic's exponentials, or, equivalently, it is MELL augmented with the non-commutative self-dual connective seq. NEL is presented in deep inference, because no Gentzen formalism can express it in such a way that the cut rule is admissible. Other recent work shows that system NEL is Turing-complete, and is able to express process algebra sequential composition directly and model causal quantum evolution faithfully. In this paper, we show cut elimination for NEL, based on a technique that we call splitting. The splitting theorem shows how and to what extent we can recover a sequent-like structure in NEL proofs. When combined with a 'decomposition' theorem, proved in the previous paper of this series, splitting yields a cut-elimination procedure for NEL.
UR - http://www.scopus.com/inward/record.url?scp=79956140311&partnerID=8YFLogxK
UR - http://journals.cambridge.org/action/displayJournal?jid=MSC
U2 - 10.1017/S096012951100003X
DO - 10.1017/S096012951100003X
M3 - Article
SN - 0960-1295
VL - 21
SP - 563
EP - 584
JO - Mathematical Structures in Computer Science
JF - Mathematical Structures in Computer Science
IS - 3
ER -