Research

A Non-commutative Extension of MELL


Reference:

Guglielmi, A. and Strassburger, L., 2002. A Non-commutative Extension of MELL. In: Logic for Programming, Artificial Intelligence, and Reasoning - 9th International Conference, LPAR, 2002-10-01.

Related documents:

This repository does not currently have the full-text of this item.
You may be able to access a copy if URLs are provided below.

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.

Details

Item Type Conference or Workshop Items (Paper)
CreatorsGuglielmi, A.and Strassburger, L.
DepartmentsFaculty of Science > Computer Science
RefereedNo
StatusPublished
ID Code5578

Export

Actions (login required)

View Item