### Abstract

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.

Original language | English |
---|---|

Pages (from-to) | 563-584 |

Number of pages | 22 |

Journal | Mathematical Structures in Computer Science |

Volume | 21 |

Issue number | 3 |

DOIs | |

Publication status | Published - Jun 2011 |

## Fingerprint Dive into the research topics of 'A system of interaction and structure V: the exponentials and splitting'. Together they form a unique fingerprint.

## Cite this

Guglielmi, A., & Straburger, L. (2011). A system of interaction and structure V: the exponentials and splitting.

*Mathematical Structures in Computer Science*,*21*(3), 563-584. https://doi.org/10.1017/S096012951100003X