InforLorV4, PascalFrancis, Corpus, bibRecord, 000730

MELL in the calculus of structures

Identifieur interne : 000730 ( PascalFrancis/Corpus ); précédent : 000729; suivant : 000731

MELL in the calculus of structures

Auteurs : Lutz Strassburger

Source :

Theoretical computer science [ 0304-3975 ] ; 2003.

RBID : Pascal:04-0108041

Descripteurs français

Pascal (Inist)
- Logique linéaire, Théorie preuve, Elimination, Décomposition, Structure, Déduction, Système, Propriété, Fragment, Contexte, Temps, Calcul structure, Elimination coupe.

English descriptors

KwdEn :
- Context, Cut elimination, Decomposition, Deduction, Elimination, Fragment, Linear logic, Proof theory, Properties, Structure, Structure calculus, System, Time.

Abstract

The calculus of structures is a new proof theoretical formalism, like natural deduction, the sequent calculus and proof nets, for specifying logical systems syntactically. In a rule in the calculus of structures, the premise as well as the conclusion are structures, which are expressions that share properties of formulae and sequents. In this paper, I study a system for MELL, the multiplicative exponential fragment of linear logic, in the calculus of structures. It has the following features: a local promotion rule, no non-deterministic splitting of the context in the times rule and a modular proof for the cut elimination theorem. Further, derivations have a new property, called decomposition, that cannot be observed in any other known proof theoretical formalism.

Notice en format standard (ISO 2709)

Pour connaître la documentation sur le format Inist Standard.

A01	`01`	`1`		`@0 0304-3975`
A02	`01`			`@0 TCSCDI`
A03		`1`		`@0 Theor. comput. sci.`
A05				`@2 309`
A06				`@2 1-3`
A08	`01`	`1`	`ENG`	`@1 MELL in the calculus of structures`
A11	`01`	`1`		`@1 STRASSBURGER (Lutz)`
A14	`01`			`@1 Loria & INRIA Lorraine, Projet Calligramme, 615 rue du Jardin Botanique @2 54602 Villers-lés-Nancy @3 FRA @Z 1 aut.`
A20				`@1 213-285`
A21				`@1 2003`
A23	`01`			`@0 ENG`
A43	`01`			`@1 INIST @2 17243 @5 354000114952080090`
A44				`@0 0000 @1 © 2004 INIST-CNRS. All rights reserved.`
A45				`@0 30 ref.`
A47	`01`	`1`		`@0 04-0108041`
A60				`@1 P`
A61				`@0 A`
A64	`01`	`1`		`@0 Theoretical computer science`
A66	`01`			`@0 NLD`
C01	`01`		`ENG`	@0 The calculus of structures is a new proof theoretical formalism, like natural deduction, the sequent calculus and proof nets, for specifying logical systems syntactically. In a rule in the calculus of structures, the premise as well as the conclusion are structures, which are expressions that share properties of formulae and sequents. In this paper, I study a system for MELL, the multiplicative exponential fragment of linear logic, in the calculus of structures. It has the following features: a local promotion rule, no non-deterministic splitting of the context in the times rule and a modular proof for the cut elimination theorem. Further, derivations have a new property, called decomposition, that cannot be observed in any other known proof theoretical formalism.
C02	`01`	`X`		`@0 001A02A01B`
C02	`02`	`X`		`@0 001A02A01F`
C03	`01`	`X`	`FRE`	`@0 Logique linéaire @5 01`
C03	`01`	`X`	`ENG`	`@0 Linear logic @5 01`
C03	`01`	`X`	`SPA`	`@0 Lógica lineal @5 01`
C03	`02`	`X`	`FRE`	`@0 Théorie preuve @5 02`
C03	`02`	`X`	`ENG`	`@0 Proof theory @5 02`
C03	`02`	`X`	`SPA`	`@0 Teoría demonstración @5 02`
C03	`03`	`X`	`FRE`	`@0 Elimination @5 03`
C03	`03`	`X`	`ENG`	`@0 Elimination @5 03`
C03	`03`	`X`	`SPA`	`@0 Eliminación @5 03`
C03	`04`	`X`	`FRE`	`@0 Décomposition @5 59`
C03	`04`	`X`	`ENG`	`@0 Decomposition @5 59`
C03	`04`	`X`	`SPA`	`@0 Descomposición @5 59`
C03	`05`	`X`	`FRE`	`@0 Structure @5 60`
C03	`05`	`X`	`ENG`	`@0 Structure @5 60`
C03	`05`	`X`	`SPA`	`@0 Estructura @5 60`
C03	`06`	`X`	`FRE`	`@0 Déduction @5 61`
C03	`06`	`X`	`ENG`	`@0 Deduction @5 61`
C03	`06`	`X`	`SPA`	`@0 Deducción @5 61`
C03	`07`	`X`	`FRE`	`@0 Système @5 62`
C03	`07`	`X`	`ENG`	`@0 System @5 62`
C03	`07`	`X`	`SPA`	`@0 Sistema @5 62`
C03	`08`	`X`	`FRE`	`@0 Propriété @5 63`
C03	`08`	`X`	`ENG`	`@0 Properties @5 63`
C03	`08`	`X`	`SPA`	`@0 Propiedad @5 63`
C03	`09`	`X`	`FRE`	`@0 Fragment @5 64`
C03	`09`	`X`	`ENG`	`@0 Fragment @5 64`
C03	`09`	`X`	`SPA`	`@0 Fragmento @5 64`
C03	`10`	`X`	`FRE`	`@0 Contexte @5 66`
C03	`10`	`X`	`ENG`	`@0 Context @5 66`
C03	`10`	`X`	`SPA`	`@0 Contexto @5 66`
C03	`11`	`X`	`FRE`	`@0 Temps @5 67`
C03	`11`	`X`	`ENG`	`@0 Time @5 67`
C03	`11`	`X`	`SPA`	`@0 Tiempo @5 67`
C03	`12`	`X`	`FRE`	`@0 Calcul structure @4 CD @5 96`
C03	`12`	`X`	`ENG`	`@0 Structure calculus @4 CD @5 96`
C03	`13`	`X`	`FRE`	`@0 Elimination coupe @4 CD @5 97`
C03	`13`	`X`	`ENG`	`@0 Cut elimination @4 CD @5 97`
N21				`@1 068`

Format Inist (serveur)

NO :	PASCAL 04-0108041 INIST
ET :	MELL in the calculus of structures
AU :	STRASSBURGER (Lutz)
AF :	Loria & INRIA Lorraine, Projet Calligramme, 615 rue du Jardin Botanique/54602 Villers-lés-Nancy/France (1 aut.)
DT :	Publication en série; Niveau analytique
SO :	Theoretical computer science; ISSN 0304-3975; Coden TCSCDI; Pays-Bas; Da. 2003; Vol. 309; No. 1-3; Pp. 213-285; Bibl. 30 ref.
LA :	Anglais
EA :	The calculus of structures is a new proof theoretical formalism, like natural deduction, the sequent calculus and proof nets, for specifying logical systems syntactically. In a rule in the calculus of structures, the premise as well as the conclusion are structures, which are expressions that share properties of formulae and sequents. In this paper, I study a system for MELL, the multiplicative exponential fragment of linear logic, in the calculus of structures. It has the following features: a local promotion rule, no non-deterministic splitting of the context in the times rule and a modular proof for the cut elimination theorem. Further, derivations have a new property, called decomposition, that cannot be observed in any other known proof theoretical formalism.
CC :	001A02A01B; 001A02A01F
FD :	Logique linéaire; Théorie preuve; Elimination; Décomposition; Structure; Déduction; Système; Propriété; Fragment; Contexte; Temps; Calcul structure; Elimination coupe
ED :	Linear logic; Proof theory; Elimination; Decomposition; Structure; Deduction; System; Properties; Fragment; Context; Time; Structure calculus; Cut elimination
SD :	Lógica lineal; Teoría demonstración; Eliminación; Descomposición; Estructura; Deducción; Sistema; Propiedad; Fragmento; Contexto; Tiempo
LO :	INIST-17243.354000114952080090
ID :	04-0108041

Links to Exploration step

Pascal:04-0108041

Le document en format XML

<record><TEI><teiHeader><fileDesc><titleStmt><title xml:lang="en" level="a">MELL in the calculus of structures</title>
<author><name sortKey="Strassburger, Lutz" sort="Strassburger, Lutz" uniqKey="Strassburger L" first="Lutz" last="Strassburger">Lutz Strassburger</name>
<affiliation><inist:fA14 i1="01"><s1>Loria & INRIA Lorraine, Projet Calligramme, 615 rue du Jardin Botanique</s1>
<s2>54602 Villers-lés-Nancy</s2>
<s3>FRA</s3>
<sZ>1 aut.</sZ>
</inist:fA14>
</affiliation>
</author>
</titleStmt>
<publicationStmt><idno type="wicri:source">INIST</idno>
<idno type="inist">04-0108041</idno>
<date when="2003">2003</date>
<idno type="stanalyst">PASCAL 04-0108041 INIST</idno>
<idno type="RBID">Pascal:04-0108041</idno>
<idno type="wicri:Area/PascalFrancis/Corpus">000730</idno>
</publicationStmt>
<sourceDesc><biblStruct><analytic><title xml:lang="en" level="a">MELL in the calculus of structures</title>
<author><name sortKey="Strassburger, Lutz" sort="Strassburger, Lutz" uniqKey="Strassburger L" first="Lutz" last="Strassburger">Lutz Strassburger</name>
<affiliation><inist:fA14 i1="01"><s1>Loria & INRIA Lorraine, Projet Calligramme, 615 rue du Jardin Botanique</s1>
<s2>54602 Villers-lés-Nancy</s2>
<s3>FRA</s3>
<sZ>1 aut.</sZ>
</inist:fA14>
</affiliation>
</author>
</analytic>
<series><title level="j" type="main">Theoretical computer science</title>
<title level="j" type="abbreviated">Theor. comput. sci.</title>
<idno type="ISSN">0304-3975</idno>
<imprint><date when="2003">2003</date>
</imprint>
</series>
</biblStruct>
</sourceDesc>
<seriesStmt><title level="j" type="main">Theoretical computer science</title>
<title level="j" type="abbreviated">Theor. comput. sci.</title>
<idno type="ISSN">0304-3975</idno>
</seriesStmt>
</fileDesc>
<profileDesc><textClass><keywords scheme="KwdEn" xml:lang="en"><term>Context</term>
<term>Cut elimination</term>
<term>Decomposition</term>
<term>Deduction</term>
<term>Elimination</term>
<term>Fragment</term>
<term>Linear logic</term>
<term>Proof theory</term>
<term>Properties</term>
<term>Structure</term>
<term>Structure calculus</term>
<term>System</term>
<term>Time</term>
</keywords>
<keywords scheme="Pascal" xml:lang="fr"><term>Logique linéaire</term>
<term>Théorie preuve</term>
<term>Elimination</term>
<term>Décomposition</term>
<term>Structure</term>
<term>Déduction</term>
<term>Système</term>
<term>Propriété</term>
<term>Fragment</term>
<term>Contexte</term>
<term>Temps</term>
<term>Calcul structure</term>
<term>Elimination coupe</term>
</keywords>
</textClass>
</profileDesc>
</teiHeader>
<front><div type="abstract" xml:lang="en">The calculus of structures is a new proof theoretical formalism, like natural deduction, the sequent calculus and proof nets, for specifying logical systems syntactically. In a rule in the calculus of structures, the premise as well as the conclusion are structures, which are expressions that share properties of formulae and sequents. In this paper, I study a system for MELL, the multiplicative exponential fragment of linear logic, in the calculus of structures. It has the following features: a local promotion rule, no non-deterministic splitting of the context in the times rule and a modular proof for the cut elimination theorem. Further, derivations have a new property, called decomposition, that cannot be observed in any other known proof theoretical formalism.</div>
</front>
</TEI>
<inist><standard h6="B"><pA><fA01 i1="01" i2="1"><s0>0304-3975</s0>
</fA01>
<fA02 i1="01"><s0>TCSCDI</s0>
</fA02>
<fA03 i2="1"><s0>Theor. comput. sci.</s0>
</fA03>
<fA05><s2>309</s2>
</fA05>
<fA06><s2>1-3</s2>
</fA06>
<fA08 i1="01" i2="1" l="ENG"><s1>MELL in the calculus of structures</s1>
</fA08>
<fA11 i1="01" i2="1"><s1>STRASSBURGER (Lutz)</s1>
</fA11>
<fA14 i1="01"><s1>Loria & INRIA Lorraine, Projet Calligramme, 615 rue du Jardin Botanique</s1>
<s2>54602 Villers-lés-Nancy</s2>
<s3>FRA</s3>
<sZ>1 aut.</sZ>
</fA14>
<fA20><s1>213-285</s1>
</fA20>
<fA21><s1>2003</s1>
</fA21>
<fA23 i1="01"><s0>ENG</s0>
</fA23>
<fA43 i1="01"><s1>INIST</s1>
<s2>17243</s2>
<s5>354000114952080090</s5>
</fA43>
<fA44><s0>0000</s0>
<s1>© 2004 INIST-CNRS. All rights reserved.</s1>
</fA44>
<fA45><s0>30 ref.</s0>
</fA45>
<fA47 i1="01" i2="1"><s0>04-0108041</s0>
</fA47>
<fA60><s1>P</s1>
</fA60>
<fA61><s0>A</s0>
</fA61>
<fA64 i1="01" i2="1"><s0>Theoretical computer science</s0>
</fA64>
<fA66 i1="01"><s0>NLD</s0>
</fA66>
<fC01 i1="01" l="ENG"><s0>The calculus of structures is a new proof theoretical formalism, like natural deduction, the sequent calculus and proof nets, for specifying logical systems syntactically. In a rule in the calculus of structures, the premise as well as the conclusion are structures, which are expressions that share properties of formulae and sequents. In this paper, I study a system for MELL, the multiplicative exponential fragment of linear logic, in the calculus of structures. It has the following features: a local promotion rule, no non-deterministic splitting of the context in the times rule and a modular proof for the cut elimination theorem. Further, derivations have a new property, called decomposition, that cannot be observed in any other known proof theoretical formalism.</s0>
</fC01>
<fC02 i1="01" i2="X"><s0>001A02A01B</s0>
</fC02>
<fC02 i1="02" i2="X"><s0>001A02A01F</s0>
</fC02>
<fC03 i1="01" i2="X" l="FRE"><s0>Logique linéaire</s0>
<s5>01</s5>
</fC03>
<fC03 i1="01" i2="X" l="ENG"><s0>Linear logic</s0>
<s5>01</s5>
</fC03>
<fC03 i1="01" i2="X" l="SPA"><s0>Lógica lineal</s0>
<s5>01</s5>
</fC03>
<fC03 i1="02" i2="X" l="FRE"><s0>Théorie preuve</s0>
<s5>02</s5>
</fC03>
<fC03 i1="02" i2="X" l="ENG"><s0>Proof theory</s0>
<s5>02</s5>
</fC03>
<fC03 i1="02" i2="X" l="SPA"><s0>Teoría demonstración</s0>
<s5>02</s5>
</fC03>
<fC03 i1="03" i2="X" l="FRE"><s0>Elimination</s0>
<s5>03</s5>
</fC03>
<fC03 i1="03" i2="X" l="ENG"><s0>Elimination</s0>
<s5>03</s5>
</fC03>
<fC03 i1="03" i2="X" l="SPA"><s0>Eliminación</s0>
<s5>03</s5>
</fC03>
<fC03 i1="04" i2="X" l="FRE"><s0>Décomposition</s0>
<s5>59</s5>
</fC03>
<fC03 i1="04" i2="X" l="ENG"><s0>Decomposition</s0>
<s5>59</s5>
</fC03>
<fC03 i1="04" i2="X" l="SPA"><s0>Descomposición</s0>
<s5>59</s5>
</fC03>
<fC03 i1="05" i2="X" l="FRE"><s0>Structure</s0>
<s5>60</s5>
</fC03>
<fC03 i1="05" i2="X" l="ENG"><s0>Structure</s0>
<s5>60</s5>
</fC03>
<fC03 i1="05" i2="X" l="SPA"><s0>Estructura</s0>
<s5>60</s5>
</fC03>
<fC03 i1="06" i2="X" l="FRE"><s0>Déduction</s0>
<s5>61</s5>
</fC03>
<fC03 i1="06" i2="X" l="ENG"><s0>Deduction</s0>
<s5>61</s5>
</fC03>
<fC03 i1="06" i2="X" l="SPA"><s0>Deducción</s0>
<s5>61</s5>
</fC03>
<fC03 i1="07" i2="X" l="FRE"><s0>Système</s0>
<s5>62</s5>
</fC03>
<fC03 i1="07" i2="X" l="ENG"><s0>System</s0>
<s5>62</s5>
</fC03>
<fC03 i1="07" i2="X" l="SPA"><s0>Sistema</s0>
<s5>62</s5>
</fC03>
<fC03 i1="08" i2="X" l="FRE"><s0>Propriété</s0>
<s5>63</s5>
</fC03>
<fC03 i1="08" i2="X" l="ENG"><s0>Properties</s0>
<s5>63</s5>
</fC03>
<fC03 i1="08" i2="X" l="SPA"><s0>Propiedad</s0>
<s5>63</s5>
</fC03>
<fC03 i1="09" i2="X" l="FRE"><s0>Fragment</s0>
<s5>64</s5>
</fC03>
<fC03 i1="09" i2="X" l="ENG"><s0>Fragment</s0>
<s5>64</s5>
</fC03>
<fC03 i1="09" i2="X" l="SPA"><s0>Fragmento</s0>
<s5>64</s5>
</fC03>
<fC03 i1="10" i2="X" l="FRE"><s0>Contexte</s0>
<s5>66</s5>
</fC03>
<fC03 i1="10" i2="X" l="ENG"><s0>Context</s0>
<s5>66</s5>
</fC03>
<fC03 i1="10" i2="X" l="SPA"><s0>Contexto</s0>
<s5>66</s5>
</fC03>
<fC03 i1="11" i2="X" l="FRE"><s0>Temps</s0>
<s5>67</s5>
</fC03>
<fC03 i1="11" i2="X" l="ENG"><s0>Time</s0>
<s5>67</s5>
</fC03>
<fC03 i1="11" i2="X" l="SPA"><s0>Tiempo</s0>
<s5>67</s5>
</fC03>
<fC03 i1="12" i2="X" l="FRE"><s0>Calcul structure</s0>
<s4>CD</s4>
<s5>96</s5>
</fC03>
<fC03 i1="12" i2="X" l="ENG"><s0>Structure calculus</s0>
<s4>CD</s4>
<s5>96</s5>
</fC03>
<fC03 i1="13" i2="X" l="FRE"><s0>Elimination coupe</s0>
<s4>CD</s4>
<s5>97</s5>
</fC03>
<fC03 i1="13" i2="X" l="ENG"><s0>Cut elimination</s0>
<s4>CD</s4>
<s5>97</s5>
</fC03>
<fN21><s1>068</s1>
</fN21>
</pA>
</standard>
<server><NO>PASCAL 04-0108041 INIST</NO>
<ET>MELL in the calculus of structures</ET>
<AU>STRASSBURGER (Lutz)</AU>
<AF>Loria & INRIA Lorraine, Projet Calligramme, 615 rue du Jardin Botanique/54602 Villers-lés-Nancy/France (1 aut.)</AF>
<DT>Publication en série; Niveau analytique</DT>
<SO>Theoretical computer science; ISSN 0304-3975; Coden TCSCDI; Pays-Bas; Da. 2003; Vol. 309; No. 1-3; Pp. 213-285; Bibl. 30 ref.</SO>
<LA>Anglais</LA>
<EA>The calculus of structures is a new proof theoretical formalism, like natural deduction, the sequent calculus and proof nets, for specifying logical systems syntactically. In a rule in the calculus of structures, the premise as well as the conclusion are structures, which are expressions that share properties of formulae and sequents. In this paper, I study a system for MELL, the multiplicative exponential fragment of linear logic, in the calculus of structures. It has the following features: a local promotion rule, no non-deterministic splitting of the context in the times rule and a modular proof for the cut elimination theorem. Further, derivations have a new property, called decomposition, that cannot be observed in any other known proof theoretical formalism.</EA>
<CC>001A02A01B; 001A02A01F</CC>
<FD>Logique linéaire; Théorie preuve; Elimination; Décomposition; Structure; Déduction; Système; Propriété; Fragment; Contexte; Temps; Calcul structure; Elimination coupe</FD>
<ED>Linear logic; Proof theory; Elimination; Decomposition; Structure; Deduction; System; Properties; Fragment; Context; Time; Structure calculus; Cut elimination</ED>
<SD>Lógica lineal; Teoría demonstración; Eliminación; Descomposición; Estructura; Deducción; Sistema; Propiedad; Fragmento; Contexto; Tiempo</SD>
<LO>INIST-17243.354000114952080090</LO>
<ID>04-0108041</ID>
</server>
</inist>
</record>

Pour manipuler ce document sous Unix (Dilib)

EXPLOR_STEP=$WICRI_ROOT/Wicri/Lorraine/explor/InforLorV4/Data/PascalFrancis/Corpus

HfdSelect -h $EXPLOR_STEP/biblio.hfd -nk 000730 | SxmlIndent | more

HfdSelect -h $EXPLOR_AREA/Data/PascalFrancis/Corpus/biblio.hfd -nk 000730 | SxmlIndent | more

Pour mettre un lien sur cette page dans le réseau Wicri

{{Explor lien
   |wiki=    Wicri/Lorraine
   |area=    InforLorV4
   |flux=    PascalFrancis
   |étape=   Corpus
   |type=    RBID
   |clé=     Pascal:04-0108041
   |texte=   MELL in the calculus of structures
}}

This area was generated with Dilib version V0.6.33.
Data generation: Mon Jun 10 21:56:28 2019. Site generation: Fri Feb 25 15:29:27 2022

	Serveur d'exploration sur la recherche en informatique en Lorraine
	Attention, ce site est en cours de développement ! Attention, site généré par des moyens informatiques à partir de corpus bruts. Les informations ne sont donc pas validées.

Serveur d'exploration sur la recherche en informatique en Lorraine

MELL in the calculus of structures

MELL in the calculus of structures

Source :

Descripteurs français

English descriptors

Abstract

Notice en format standard (ISO 2709)

Format Inist (serveur)

Links to Exploration step

Le document en format XML

Pour manipuler ce document sous Unix (Dilib)

Pour mettre un lien sur cette page dans le réseau Wicri