Natural Deduction and Normalisation for Partially Commutative Linear Logic and Lambek Calculus with Product

Maxime Amblard; Christian Retoré

hal-00409486, version 1

Natural Deduction and Normalisation for Partially Commutative Linear Logic and Lambek Calculus with Product

Maxime Amblard ^1, 2, Christian Retoré (, ) ^1, 2

Computation and Logic in the Real World (Computing in Europe 2007) (2007) 28--44

Abstract: This paper provides a natural deduction system for Partially Commutative Intuitionistic Multiplicative Linear Logic (PCIMLL) and establishes its normalisation and subformula property. Such a system in- volves both commutative and non commutative connectives and deals with context that are series-parallel multisets of formulæ. This calcu- lus is the extension of the one introduced by de Groote presented by the second order for modelling Petri net execution, with a full entropy which allow order to be relaxed into any suborder — as opposed to the Non Commutative Logic of Abrusci and Ruet. Our result also includes, as a special case, the normalisation of natural deduction the Lambek calculus with product, which is unsurprising but yet unproved. Up to now PCIMLL with full entropy had no natural deduction. In particular for linguistic applications, such a syntax is much welcome to construct semantic representations from syntactic analyses.

1: Laboratoire Bordelais de Recherche en Informatique (LaBRI)
CNRS : UMR5800 – Université Sciences et Technologies - Bordeaux I – École Nationale Supérieure d'Électronique, Informatique et Radiocommunications de Bordeaux (ENSEIRB) – Université Victor Segalen - Bordeaux II
2: SIGNES (INRIA Futurs)
INRIA – CNRS : UMR5800 – Université Sciences et Technologies - Bordeaux I – Université Michel de Montaigne - Bordeaux III – École Nationale Supérieure d'Électronique, Informatique et Radiocommunications de Bordeaux (ENSEIRB)

hal-00409486, version 1
http://hal.archives-ouvertes.fr/hal-00409486
oai:hal.archives-ouvertes.fr:hal-00409486
From: Christian Retore <>
Submitted on: Monday, 14 September 2009 02:05:14
Updated on: Tuesday, 22 September 2009 10:27:51

See detailed view

Associated documents

PDF :

Export

Bibtex EndNote TEI RefWorks

%% hal-00409486, version 1
%% http://hal.archives-ouvertes.fr/hal-00409486
@inproceedings{amblard:hal-00409486,
    hal_id = {hal-00409486},
    url = {http://hal.archives-ouvertes.fr/hal-00409486},
    title = {{Natural Deduction and Normalisation for Partially Commutative Linear Logic and Lambek Calculus with Product}},
    author = {Amblard, Maxime and Retor{\'e}, Christian},
    abstract = {{This paper provides a natural deduction system for Partially Commutative Intuitionistic Multiplicative Linear Logic (PCIMLL) and establishes its normalisation and subformula property. Such a system in- volves both commutative and non commutative connectives and deals with context that are series-parallel multisets of formul{\ae}. This calcu- lus is the extension of the one introduced by de Groote presented by the second order for modelling Petri net execution, with a full entropy which allow order to be relaxed into any suborder - as opposed to the Non Commutative Logic of Abrusci and Ruet. Our result also includes, as a special case, the normalisation of natural deduction the Lambek calculus with product, which is unsurprising but yet unproved. Up to now PCIMLL with full entropy had no natural deduction. In particular for linguistic applications, such a syntax is much welcome to construct semantic representations from syntactic analyses.}},
    keywords = {logi;, proof theory; linear logic; Lambek calculus},
    language = {English},
    affiliation = {Laboratoire Bordelais de Recherche en Informatique - LaBRI , SIGNES - INRIA Futurs},
    booktitle = {{Computation and Logic in the Real World (Computing in Europe 2007)}},
    publisher = {Universit{\`a} di Siena},
    pages = {28--44},
    address = {Siena, Italy},
    editor = {S. B. Cooper and T. F. Kent and B. L{\"o}we and A. Sorbi },
    number = {ID487 },
    series = {Quaderni del Dipartimento di Scienze Matematiche e Informatiche "Roberto Magari" },
    audience = {international },
    year = {2007},
    month = Jun,
    pdf = {http://hal.archives-ouvertes.fr/hal-00409486/PDF/amblard\_retore\_cie.pdf},
}

<?xml version="1.0" encoding="UTF-8"?>
<listBibl xmlns="http://www.tei-c.org/ns/1.0" xmlns:xlink="http://www.w3.org/1999/xlink" xmlns:mml="http://www.w3.org/1998/Math/MathML">
<listBibl type="inproceedings"><head>Peer-reviewed conferences/proceedings</head>
<biblStruct type="inproceedings" xml:id="hal-00409486"><analytic>
<author><persName><forename>Maxime</forename><surname>Amblard</surname></persName>
<affiliation>
<orgName type="laboratory">LaBRI</orgName>
<orgName type="team">Laboratoire Bordelais de Recherche en Informatique</orgName>
<country>FR</country>
<orgName type="institution">CNRS : UMR5800</orgName>
<orgName type="institution">Université Sciences et Technologies - Bordeaux I</orgName>
<orgName type="institution">École Nationale Supérieure d'Électronique, Informatique et Radiocommunications de Bordeaux (ENSEIRB)</orgName>
<orgName type="institution">Université Victor Segalen - Bordeaux II</orgName>
</affiliation>
<affiliation>
<orgName type="laboratory">INRIA Futurs</orgName>
<orgName type="team">SIGNES</orgName>
<country>FR</country>
<orgName type="institution">INRIA</orgName>
<orgName type="institution">CNRS : UMR5800</orgName>
<orgName type="institution">Université Sciences et Technologies - Bordeaux I</orgName>
<orgName type="institution">Université Michel de Montaigne - Bordeaux III</orgName>
<orgName type="institution">École Nationale Supérieure d'Électronique, Informatique et Radiocommunications de Bordeaux (ENSEIRB)</orgName>
</affiliation>
</author>
<author><persName><forename>Christian</forename><surname>Retoré</surname></persName>
<affiliation>
<orgName type="laboratory">LaBRI</orgName>
<orgName type="team">Laboratoire Bordelais de Recherche en Informatique</orgName>
<country>FR</country>
<orgName type="institution">CNRS : UMR5800</orgName>
<orgName type="institution">Université Sciences et Technologies - Bordeaux I</orgName>
<orgName type="institution">École Nationale Supérieure d'Électronique, Informatique et Radiocommunications de Bordeaux (ENSEIRB)</orgName>
<orgName type="institution">Université Victor Segalen - Bordeaux II</orgName>
</affiliation>
<affiliation>
<orgName type="laboratory">INRIA Futurs</orgName>
<orgName type="team">SIGNES</orgName>
<country>FR</country>
<orgName type="institution">INRIA</orgName>
<orgName type="institution">CNRS : UMR5800</orgName>
<orgName type="institution">Université Sciences et Technologies - Bordeaux I</orgName>
<orgName type="institution">Université Michel de Montaigne - Bordeaux III</orgName>
<orgName type="institution">École Nationale Supérieure d'Électronique, Informatique et Radiocommunications de Bordeaux (ENSEIRB)</orgName>
</affiliation>
</author>
<title type="main" level="a">Natural Deduction and Normalisation for Partially Commutative Linear Logic and Lambek Calculus with Product</title></analytic><monogr><title level="m" type="main">Computation and Logic in the Real World (Computing in Europe 2007)</title><meeting>Computation and Logic in the Real World (Computing in Europe 2007)</meeting><imprint><publisher>Università di Siena</publisher><pubPlace><settlement>Siena</settlement><country>Italy</country></pubPlace><biblScope type="publicationDate">2007-06-18</biblScope><biblScope type="issue">ID487</biblScope><biblScope type="pp">28--44</biblScope></imprint></monogr><idno type="HALid">http://hal.archives-ouvertes.fr/hal-00409486</idno><idno type="HALFile">http://hal.archives-ouvertes.fr/hal-00409486/PDF/amblard_retore_cie.pdf</idno></biblStruct>
</listBibl>
</listBibl>