InforLorV4, Main, Curation, bibRecord, 007A83

Connection-Based Proof Construction in Non-commutative Logic

Identifieur interne : 007A83 ( Main/Curation ); précédent : 007A82; suivant : 007A84

Connection-Based Proof Construction in Non-commutative Logic

Auteurs : D. Galmiche [France] ; J. M. Notin [France]

Source :

Lecture Notes in Computer Science [ 0302-9743 ]

RBID : ISTEX:0DCF7396E9D9B84A9FE7C582A039BFA9C1E7C28A

Descripteurs français

Pascal (Inist)
- Etiquette, Logique linéaire, Logique multiplicative, Polarisation, Programmation logique, Réseau preuve.

English descriptors

KwdEn :
- Label, Linear logic, Logical programming, Multiplicative logic, Polarization, Proof net.

Abstract

Abstract.: We propose a connection-based characterization of the multiplicative fragment of non-commutative logic (MNL), that is a conservative extension of both commutative (MLL) and non-commutative or cyclic (MCyLL) linear logic. It is based on a characterization for MLL together with the introduction of labels and constraints from a formula polarization process. We also study a similar characterization for the intuitionistic fragment of MNL. Finally, we consider the relationships between these results and proof nets construction in MNL based on labels and constraints.

Url:

https://api.istex.fr/ark:/67375/HCB-39W1GLVN-9/fulltext.pdf

DOI: 10.1007/978-3-540-39813-4_30

Links toward previous steps (curation, corpus...)

to stream Istex, to step Corpus: Pour aller vers cette notice dans l'étape Curation :000301
to stream Istex, to step Curation: Pour aller vers cette notice dans l'étape Curation :000300
to stream Istex, to step Checkpoint: Pour aller vers cette notice dans l'étape Curation :001A73
to stream Main, to step Merge: Pour aller vers cette notice dans l'étape Curation :007E62
to stream PascalFrancis, to step Corpus: Pour aller vers cette notice dans l'étape Curation :000698
to stream PascalFrancis, to step Curation: Pour aller vers cette notice dans l'étape Curation :000343
to stream PascalFrancis, to step Checkpoint: Pour aller vers cette notice dans l'étape Curation :000717
to stream Main, to step Merge: Pour aller vers cette notice dans l'étape Curation :007F76

Links to Exploration step

ISTEX:0DCF7396E9D9B84A9FE7C582A039BFA9C1E7C28A

Le document en format XML

<record><TEI wicri:istexFullTextTei="biblStruct"><teiHeader><fileDesc><titleStmt><title xml:lang="en">Connection-Based Proof Construction in Non-commutative Logic</title>
<author><name sortKey="Galmiche, D" sort="Galmiche, D" uniqKey="Galmiche D" first="D." last="Galmiche">D. Galmiche</name>
</author>
<author><name sortKey="Notin, J M" sort="Notin, J M" uniqKey="Notin J" first="J. M." last="Notin">J. M. Notin</name>
</author>
</titleStmt>
<publicationStmt><idno type="wicri:source">ISTEX</idno>
<idno type="RBID">ISTEX:0DCF7396E9D9B84A9FE7C582A039BFA9C1E7C28A</idno>
<date when="2003" year="2003">2003</date>
<idno type="doi">10.1007/978-3-540-39813-4_30</idno>
<idno type="url">https://api.istex.fr/ark:/67375/HCB-39W1GLVN-9/fulltext.pdf</idno>
<idno type="wicri:Area/Istex/Corpus">000301</idno>
<idno type="wicri:explorRef" wicri:stream="Istex" wicri:step="Corpus" wicri:corpus="ISTEX">000301</idno>
<idno type="wicri:Area/Istex/Curation">000300</idno>
<idno type="wicri:Area/Istex/Checkpoint">001A73</idno>
<idno type="wicri:explorRef" wicri:stream="Istex" wicri:step="Checkpoint">001A73</idno>
<idno type="wicri:doubleKey">0302-9743:2003:Galmiche D:connection:based:proof</idno>
<idno type="wicri:Area/Main/Merge">007E62</idno>
<idno type="wicri:source">INIST</idno>
<idno type="RBID">Pascal:04-0200594</idno>
<idno type="wicri:Area/PascalFrancis/Corpus">000698</idno>
<idno type="wicri:Area/PascalFrancis/Curation">000343</idno>
<idno type="wicri:Area/PascalFrancis/Checkpoint">000717</idno>
<idno type="wicri:explorRef" wicri:stream="PascalFrancis" wicri:step="Checkpoint">000717</idno>
<idno type="wicri:doubleKey">0302-9743:2003:Galmiche D:connection:based:proof</idno>
<idno type="wicri:Area/Main/Merge">007F76</idno>
<idno type="wicri:Area/Main/Curation">007A83</idno>
</publicationStmt>
<sourceDesc><biblStruct><analytic><title level="a" type="main" xml:lang="en">Connection-Based Proof Construction in Non-commutative Logic</title>
<author><name sortKey="Galmiche, D" sort="Galmiche, D" uniqKey="Galmiche D" first="D." last="Galmiche">D. Galmiche</name>
<affiliation wicri:level="4"><country xml:lang="fr">France</country>
<wicri:regionArea>LORIA – Université Henri Poincaré, 54506, Vandœuvre-lés-Nancy Cedex</wicri:regionArea>
<placeName><region type="region" nuts="2">Grand Est</region>
<region type="old region" nuts="2">Lorraine (région)</region>
<settlement type="city">Vandœuvre-lès-Nancy</settlement>
</placeName>
<orgName type="university">Université Henri Poincaré</orgName>
</affiliation>
<affiliation wicri:level="1"><country wicri:rule="url">France</country>
</affiliation>
</author>
<author><name sortKey="Notin, J M" sort="Notin, J M" uniqKey="Notin J" first="J. M." last="Notin">J. M. Notin</name>
<affiliation wicri:level="4"><country xml:lang="fr">France</country>
<wicri:regionArea>LORIA – Université Henri Poincaré, 54506, Vandœuvre-lés-Nancy Cedex</wicri:regionArea>
<placeName><region type="region" nuts="2">Grand Est</region>
<region type="old region" nuts="2">Lorraine (région)</region>
<settlement type="city">Vandœuvre-lès-Nancy</settlement>
</placeName>
<orgName type="university">Université Henri Poincaré</orgName>
</affiliation>
<affiliation wicri:level="1"><country wicri:rule="url">France</country>
</affiliation>
</author>
</analytic>
<monogr></monogr>
<series><title level="s" type="main" xml:lang="en">Lecture Notes in Computer Science</title>
<idno type="ISSN">0302-9743</idno>
<idno type="eISSN">1611-3349</idno>
<idno type="ISSN">0302-9743</idno>
</series>
</biblStruct>
</sourceDesc>
<seriesStmt><idno type="ISSN">0302-9743</idno>
</seriesStmt>
</fileDesc>
<profileDesc><textClass><keywords scheme="KwdEn" xml:lang="en"><term>Label</term>
<term>Linear logic</term>
<term>Logical programming</term>
<term>Multiplicative logic</term>
<term>Polarization</term>
<term>Proof net</term>
</keywords>
<keywords scheme="Pascal" xml:lang="fr"><term>Etiquette</term>
<term>Logique linéaire</term>
<term>Logique multiplicative</term>
<term>Polarisation</term>
<term>Programmation logique</term>
<term>Réseau preuve</term>
</keywords>
</textClass>
</profileDesc>
</teiHeader>
<front><div type="abstract" xml:lang="en">Abstract.: We propose a connection-based characterization of the multiplicative fragment of non-commutative logic (MNL), that is a conservative extension of both commutative (MLL) and non-commutative or cyclic (MCyLL) linear logic. It is based on a characterization for MLL together with the introduction of labels and constraints from a formula polarization process. We also study a similar characterization for the intuitionistic fragment of MNL. Finally, we consider the relationships between these results and proof nets construction in MNL based on labels and constraints.</div>
</front>
</TEI>
<double idat="0302-9743:2003:Galmiche D:connection:based:proof"><INIST><TEI><teiHeader><fileDesc><titleStmt><title xml:lang="en" level="a">Connection-based proof construction in non-commutative logic</title>
<author><name sortKey="Galmiche, D" sort="Galmiche, D" uniqKey="Galmiche D" first="D." last="Galmiche">D. Galmiche</name>
<affiliation wicri:level="4"><inist:fA14 i1="01"><s1>LORIA - Université Henri Poincaré</s1>
<s2>54506 Vandœuvre-lès-Nancy</s2>
<s3>FRA</s3>
<sZ>1 aut.</sZ>
<sZ>2 aut.</sZ>
</inist:fA14>
<country>France</country>
<placeName><region type="region" nuts="2">Grand Est</region>
<region type="old region" nuts="2">Lorraine (région)</region>
<settlement type="city">Vandœuvre-lès-Nancy</settlement>
</placeName>
<orgName type="university">Université Henri Poincaré</orgName>
</affiliation>
</author>
<author><name sortKey="Notin, J M" sort="Notin, J M" uniqKey="Notin J" first="J.-M." last="Notin">J.-M. Notin</name>
<affiliation wicri:level="4"><inist:fA14 i1="01"><s1>LORIA - Université Henri Poincaré</s1>
<s2>54506 Vandœuvre-lès-Nancy</s2>
<s3>FRA</s3>
<sZ>1 aut.</sZ>
<sZ>2 aut.</sZ>
</inist:fA14>
<country>France</country>
<placeName><region type="region" nuts="2">Grand Est</region>
<region type="old region" nuts="2">Lorraine (région)</region>
<settlement type="city">Vandœuvre-lès-Nancy</settlement>
</placeName>
<orgName type="university">Université Henri Poincaré</orgName>
</affiliation>
</author>
</titleStmt>
<publicationStmt><idno type="wicri:source">INIST</idno>
<idno type="inist">04-0200594</idno>
<date when="2003">2003</date>
<idno type="stanalyst">PASCAL 04-0200594 INIST</idno>
<idno type="RBID">Pascal:04-0200594</idno>
<idno type="wicri:Area/PascalFrancis/Corpus">000698</idno>
<idno type="wicri:Area/PascalFrancis/Curation">000343</idno>
<idno type="wicri:Area/PascalFrancis/Checkpoint">000717</idno>
<idno type="wicri:explorRef" wicri:stream="PascalFrancis" wicri:step="Checkpoint">000717</idno>
<idno type="wicri:doubleKey">0302-9743:2003:Galmiche D:connection:based:proof</idno>
<idno type="wicri:Area/Main/Merge">007F76</idno>
</publicationStmt>
<sourceDesc><biblStruct><analytic><title xml:lang="en" level="a">Connection-based proof construction in non-commutative logic</title>
<author><name sortKey="Galmiche, D" sort="Galmiche, D" uniqKey="Galmiche D" first="D." last="Galmiche">D. Galmiche</name>
<affiliation wicri:level="4"><inist:fA14 i1="01"><s1>LORIA - Université Henri Poincaré</s1>
<s2>54506 Vandœuvre-lès-Nancy</s2>
<s3>FRA</s3>
<sZ>1 aut.</sZ>
<sZ>2 aut.</sZ>
</inist:fA14>
<country>France</country>
<placeName><region type="region" nuts="2">Grand Est</region>
<region type="old region" nuts="2">Lorraine (région)</region>
<settlement type="city">Vandœuvre-lès-Nancy</settlement>
</placeName>
<orgName type="university">Université Henri Poincaré</orgName>
</affiliation>
</author>
<author><name sortKey="Notin, J M" sort="Notin, J M" uniqKey="Notin J" first="J.-M." last="Notin">J.-M. Notin</name>
<affiliation wicri:level="4"><inist:fA14 i1="01"><s1>LORIA - Université Henri Poincaré</s1>
<s2>54506 Vandœuvre-lès-Nancy</s2>
<s3>FRA</s3>
<sZ>1 aut.</sZ>
<sZ>2 aut.</sZ>
</inist:fA14>
<country>France</country>
<placeName><region type="region" nuts="2">Grand Est</region>
<region type="old region" nuts="2">Lorraine (région)</region>
<settlement type="city">Vandœuvre-lès-Nancy</settlement>
</placeName>
<orgName type="university">Université Henri Poincaré</orgName>
</affiliation>
</author>
</analytic>
<series><title level="j" type="main">Lecture notes in computer science</title>
<idno type="ISSN">0302-9743</idno>
<imprint><date when="2003">2003</date>
</imprint>
</series>
</biblStruct>
</sourceDesc>
<seriesStmt><title level="j" type="main">Lecture notes in computer science</title>
<idno type="ISSN">0302-9743</idno>
</seriesStmt>
</fileDesc>
<profileDesc><textClass><keywords scheme="KwdEn" xml:lang="en"><term>Label</term>
<term>Linear logic</term>
<term>Logical programming</term>
<term>Multiplicative logic</term>
<term>Polarization</term>
<term>Proof net</term>
</keywords>
<keywords scheme="Pascal" xml:lang="fr"><term>Programmation logique</term>
<term>Logique linéaire</term>
<term>Etiquette</term>
<term>Polarisation</term>
<term>Logique multiplicative</term>
<term>Réseau preuve</term>
</keywords>
</textClass>
</profileDesc>
</teiHeader>
<front><div type="abstract" xml:lang="en">We propose a connection-based characterization of the multiplicative fragment of non-commutative logic (MNL), that is a conservative extension of both commutative (MLL) and non-commutative or cyclic (MCyLL) linear logic. It is based on a characterization for MLL together with the introduction of labels and constraints from a formula polarization process. We also study a similar characterization for the intuitionistic fragment of MNL. Finally, we consider the relationships between these results and proof nets construction in MNL based on labels and constraints.</div>
</front>
</TEI>
</INIST>
<ISTEX><TEI wicri:istexFullTextTei="biblStruct"><teiHeader><fileDesc><titleStmt><title xml:lang="en">Connection-Based Proof Construction in Non-commutative Logic</title>
<author><name sortKey="Galmiche, D" sort="Galmiche, D" uniqKey="Galmiche D" first="D." last="Galmiche">D. Galmiche</name>
</author>
<author><name sortKey="Notin, J M" sort="Notin, J M" uniqKey="Notin J" first="J. M." last="Notin">J. M. Notin</name>
</author>
</titleStmt>
<publicationStmt><idno type="wicri:source">ISTEX</idno>
<idno type="RBID">ISTEX:0DCF7396E9D9B84A9FE7C582A039BFA9C1E7C28A</idno>
<date when="2003" year="2003">2003</date>
<idno type="doi">10.1007/978-3-540-39813-4_30</idno>
<idno type="url">https://api.istex.fr/ark:/67375/HCB-39W1GLVN-9/fulltext.pdf</idno>
<idno type="wicri:Area/Istex/Corpus">000301</idno>
<idno type="wicri:explorRef" wicri:stream="Istex" wicri:step="Corpus" wicri:corpus="ISTEX">000301</idno>
<idno type="wicri:Area/Istex/Curation">000300</idno>
<idno type="wicri:Area/Istex/Checkpoint">001A73</idno>
<idno type="wicri:explorRef" wicri:stream="Istex" wicri:step="Checkpoint">001A73</idno>
<idno type="wicri:doubleKey">0302-9743:2003:Galmiche D:connection:based:proof</idno>
<idno type="wicri:Area/Main/Merge">007E62</idno>
</publicationStmt>
<sourceDesc><biblStruct><analytic><title level="a" type="main" xml:lang="en">Connection-Based Proof Construction in Non-commutative Logic</title>
<author><name sortKey="Galmiche, D" sort="Galmiche, D" uniqKey="Galmiche D" first="D." last="Galmiche">D. Galmiche</name>
<affiliation wicri:level="4"><country xml:lang="fr">France</country>
<wicri:regionArea>LORIA – Université Henri Poincaré, 54506, Vandœuvre-lés-Nancy Cedex</wicri:regionArea>
<placeName><region type="region" nuts="2">Grand Est</region>
<region type="old region" nuts="2">Lorraine (région)</region>
<settlement type="city">Vandœuvre-lès-Nancy</settlement>
</placeName>
<orgName type="university">Université Henri Poincaré</orgName>
</affiliation>
<affiliation wicri:level="1"><country wicri:rule="url">France</country>
</affiliation>
</author>
<author><name sortKey="Notin, J M" sort="Notin, J M" uniqKey="Notin J" first="J. M." last="Notin">J. M. Notin</name>
<affiliation wicri:level="4"><country xml:lang="fr">France</country>
<wicri:regionArea>LORIA – Université Henri Poincaré, 54506, Vandœuvre-lés-Nancy Cedex</wicri:regionArea>
<placeName><region type="region" nuts="2">Grand Est</region>
<region type="old region" nuts="2">Lorraine (région)</region>
<settlement type="city">Vandœuvre-lès-Nancy</settlement>
</placeName>
<orgName type="university">Université Henri Poincaré</orgName>
</affiliation>
<affiliation wicri:level="1"><country wicri:rule="url">France</country>
</affiliation>
</author>
</analytic>
<monogr></monogr>
<series><title level="s" type="main" xml:lang="en">Lecture Notes in Computer Science</title>
<idno type="ISSN">0302-9743</idno>
<idno type="eISSN">1611-3349</idno>
<idno type="ISSN">0302-9743</idno>
</series>
</biblStruct>
</sourceDesc>
<seriesStmt><idno type="ISSN">0302-9743</idno>
</seriesStmt>
</fileDesc>
<profileDesc><textClass></textClass>
</profileDesc>
</teiHeader>
<front><div type="abstract" xml:lang="en">Abstract.: We propose a connection-based characterization of the multiplicative fragment of non-commutative logic (MNL), that is a conservative extension of both commutative (MLL) and non-commutative or cyclic (MCyLL) linear logic. It is based on a characterization for MLL together with the introduction of labels and constraints from a formula polarization process. We also study a similar characterization for the intuitionistic fragment of MNL. Finally, we consider the relationships between these results and proof nets construction in MNL based on labels and constraints.</div>
</front>
</TEI>
</ISTEX>
</double>
</record>

Pour manipuler ce document sous Unix (Dilib)

EXPLOR_STEP=$WICRI_ROOT/Wicri/Lorraine/explor/InforLorV4/Data/Main/Curation

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

HfdSelect -h $EXPLOR_AREA/Data/Main/Curation/biblio.hfd -nk 007A83 | SxmlIndent | more

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

{{Explor lien
   |wiki=    Wicri/Lorraine
   |area=    InforLorV4
   |flux=    Main
   |étape=   Curation
   |type=    RBID
   |clé=     ISTEX:0DCF7396E9D9B84A9FE7C582A039BFA9C1E7C28A
   |texte=   Connection-Based Proof Construction in Non-commutative Logic
}}

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

Connection-Based Proof Construction in Non-commutative Logic

Connection-Based Proof Construction in Non-commutative Logic

Source :

Descripteurs français

English descriptors

Abstract

Links toward previous steps (curation, corpus...)

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