A Non-commutative Extension of MELL

A Guglielmi, L Strassburger

Research output: Contribution to conferencePaper

18 Citations (Scopus)

Abstract

We extend multiplicative exponential linear logic (MELL) by a non-commutative, 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 should then be able to extend the range of applications of MELL, 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.
Original languageEnglish
Pages231-246
Number of pages16
Publication statusPublished - Oct 2002
EventLogic for Programming, Artificial Intelligence, and Reasoning - 9th International Conference, LPAR -
Duration: 1 Oct 2002 → …

Conference

ConferenceLogic for Programming, Artificial Intelligence, and Reasoning - 9th International Conference, LPAR
Period1/10/02 → …

Fingerprint Dive into the research topics of 'A Non-commutative Extension of MELL'. Together they form a unique fingerprint.

  • Cite this

    Guglielmi, A., & Strassburger, L. (2002). A Non-commutative Extension of MELL. 231-246. Paper presented at Logic for Programming, Artificial Intelligence, and Reasoning - 9th International Conference, LPAR, .