InforLorV4, Main, Curation, bibRecord, 00A844

From multiple sequent for additive linear logic to decision procedures for free lattices

Identifieur interne : 00A844 ( Main/Curation ); précédent : 00A843; suivant : 00A845

From multiple sequent for additive linear logic to decision procedures for free lattices

Auteurs : Jean-Yves Marion [France]

Source :

Theoretical Computer Science [ 0304-3975 ] ; 1999.

RBID : ISTEX:8085993A8FC74D69CBBC4756251EBEE223170CB4

Descripteurs français

Pascal (Inist)
- Calcul propositionnel, Complexité calcul, Logique mathématique, Logique propositionnelle, Théorie décision, Treillis.
mix :
- additive linear logic, calcul des séquents, decision procedure, fragment additif, free lattices, logique linéaire, problème de décision, sequent calculus, treillis libre.

English descriptors

Abstract

Abstract: The additive fragment of linear logic is complete for general (nondistributive) lattices. A sequent calculus for general lattices is presented with multiple antecedents and succedents. This construction is extended to give a sequent calculus for prepositional linear logic with both additive and multiplicative contexts. Then, various decision procedures are investigated for general lattices.

Url:

DOI: 10.1016/S0304-3975(98)00311-9

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

to stream Istex, to step Corpus: Pour aller vers cette notice dans l'étape Curation :001D83
to stream Istex, to step Curation: Pour aller vers cette notice dans l'étape Curation :001D60
to stream Istex, to step Checkpoint: Pour aller vers cette notice dans l'étape Curation :002229
to stream Main, to step Merge: Pour aller vers cette notice dans l'étape Curation :00AE96
to stream Hal, to step Corpus: Pour aller vers cette notice dans l'étape Curation :002492
to stream Hal, to step Curation: Pour aller vers cette notice dans l'étape Curation :002492
to stream Hal, to step Checkpoint: Pour aller vers cette notice dans l'étape Curation :006652
to stream Main, to step Merge: Pour aller vers cette notice dans l'étape Curation :00B431
to stream PascalFrancis, to step Corpus: Pour aller vers cette notice dans l'étape Curation :000B00
to stream PascalFrancis, to step Curation: Pour aller vers cette notice dans l'étape Curation :000D70
to stream PascalFrancis, to step Checkpoint: Pour aller vers cette notice dans l'étape Curation :000A83
to stream Main, to step Merge: Pour aller vers cette notice dans l'étape Curation :00B171

Links to Exploration step

ISTEX:8085993A8FC74D69CBBC4756251EBEE223170CB4

Le document en format XML

<record><TEI wicri:istexFullTextTei="biblStruct"><teiHeader><fileDesc><titleStmt><title>From multiple sequent for additive linear logic to decision procedures for free lattices</title>
<author><name sortKey="Marion, Jean Yves" sort="Marion, Jean Yves" uniqKey="Marion J" first="Jean-Yves" last="Marion">Jean-Yves Marion</name>
</author>
</titleStmt>
<publicationStmt><idno type="wicri:source">ISTEX</idno>
<idno type="RBID">ISTEX:8085993A8FC74D69CBBC4756251EBEE223170CB4</idno>
<date when="1999" year="1999">1999</date>
<idno type="doi">10.1016/S0304-3975(98)00311-9</idno>
<idno type="url">https://api.istex.fr/ark:/67375/6H6-N5RQFN93-0/fulltext.pdf</idno>
<idno type="wicri:Area/Istex/Corpus">001D83</idno>
<idno type="wicri:explorRef" wicri:stream="Istex" wicri:step="Corpus" wicri:corpus="ISTEX">001D83</idno>
<idno type="wicri:Area/Istex/Curation">001D60</idno>
<idno type="wicri:Area/Istex/Checkpoint">002229</idno>
<idno type="wicri:explorRef" wicri:stream="Istex" wicri:step="Checkpoint">002229</idno>
<idno type="wicri:doubleKey">0304-3975:1999:Marion J:from:multiple:sequent</idno>
<idno type="wicri:Area/Main/Merge">00AE96</idno>
<idno type="wicri:source">HAL</idno>
<idno type="RBID">Hal:inria-00098803</idno>
<idno type="url">https://hal.inria.fr/inria-00098803</idno>
<idno type="wicri:Area/Hal/Corpus">002492</idno>
<idno type="wicri:Area/Hal/Curation">002492</idno>
<idno type="wicri:Area/Hal/Checkpoint">006652</idno>
<idno type="wicri:explorRef" wicri:stream="Hal" wicri:step="Checkpoint">006652</idno>
<idno type="wicri:doubleKey">0304-3975:1999:Marion J:from:multiple:sequent</idno>
<idno type="wicri:Area/Main/Merge">00B431</idno>
<idno type="wicri:source">INIST</idno>
<idno type="RBID">Pascal:99-0463969</idno>
<idno type="wicri:Area/PascalFrancis/Corpus">000B00</idno>
<idno type="wicri:Area/PascalFrancis/Curation">000D70</idno>
<idno type="wicri:Area/PascalFrancis/Checkpoint">000A83</idno>
<idno type="wicri:explorRef" wicri:stream="PascalFrancis" wicri:step="Checkpoint">000A83</idno>
<idno type="wicri:doubleKey">0304-3975:1999:Marion J:from:multiple:sequent</idno>
<idno type="wicri:Area/Main/Merge">00B171</idno>
<idno type="wicri:Area/Main/Curation">00A844</idno>
</publicationStmt>
<sourceDesc><biblStruct><analytic><title level="a">From multiple sequent for additive linear logic to decision procedures for free lattices</title>
<author><name sortKey="Marion, Jean Yves" sort="Marion, Jean Yves" uniqKey="Marion J" first="Jean-Yves" last="Marion">Jean-Yves Marion</name>
<affiliation wicri:level="4"><country xml:lang="fr">France</country>
<wicri:regionArea>Université Nancy 2, Loria, Projet Calligramme, Campus Scientifique — B.P. 239, 54506 Vandoeuvre-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é Nancy 2</orgName>
</affiliation>
<affiliation wicri:level="1"><country wicri:rule="url">France</country>
</affiliation>
</author>
</analytic>
<monogr></monogr>
<series><title level="j">Theoretical Computer Science</title>
<title level="j" type="abbrev">TCS</title>
<idno type="ISSN">0304-3975</idno>
<imprint><publisher>ELSEVIER</publisher>
<date type="published" when="1999">1999</date>
<biblScope unit="volume">224</biblScope>
<biblScope unit="issue">1–2</biblScope>
<biblScope unit="page" from="157">157</biblScope>
<biblScope unit="page" to="172">172</biblScope>
</imprint>
<idno type="ISSN">0304-3975</idno>
</series>
</biblStruct>
</sourceDesc>
<seriesStmt><idno type="ISSN">0304-3975</idno>
</seriesStmt>
</fileDesc>
<profileDesc><textClass><keywords scheme="KwdEn" xml:lang="en"><term>Computational complexity</term>
<term>Decision theory</term>
<term>Lattice</term>
<term>Mathematical logic</term>
<term>Propositional calculus</term>
<term>Propositional logic</term>
</keywords>
<keywords scheme="Pascal" xml:lang="fr"><term>Calcul propositionnel</term>
<term>Complexité calcul</term>
<term>Logique mathématique</term>
<term>Logique propositionnelle</term>
<term>Théorie décision</term>
<term>Treillis</term>
</keywords>
<keywords scheme="Teeft" xml:lang="en"><term>Additive</term>
<term>Additive context</term>
<term>Additive contexts</term>
<term>Additive fragment</term>
<term>Additive implication</term>
<term>Algorithm</term>
<term>Calculus</term>
<term>Classical propositional logic</term>
<term>Computer science</term>
<term>Connector</term>
<term>Decision procedure</term>
<term>Decision procedures</term>
<term>Distributive lattices</term>
<term>Elsevier science</term>
<term>Free lattice</term>
<term>Free lattices</term>
<term>Free proof</term>
<term>General lattices</term>
<term>Intuitionistic</term>
<term>Last rule</term>
<term>Lattice</term>
<term>Lattice theory</term>
<term>Least element</term>
<term>Lecture notes</term>
<term>Linear logic</term>
<term>Mall</term>
<term>Multiple antecedents</term>
<term>Multiple calculus</term>
<term>Multiple sequent</term>
<term>Multiplicative</term>
<term>Multiplicative contexts</term>
<term>Other hand</term>
<term>Polynomial time</term>
<term>Propositional</term>
<term>Right rule</term>
<term>Right rules</term>
<term>Right side</term>
<term>Same atom</term>
<term>Search space</term>
<term>Seminal work</term>
<term>Sequent</term>
<term>Sequent calculus</term>
<term>Single formula</term>
<term>Structural rules</term>
<term>Theoretical computer science</term>
</keywords>
<keywords scheme="mix" xml:lang="fr"><term>additive linear logic</term>
<term>calcul des séquents</term>
<term>decision procedure</term>
<term>fragment additif</term>
<term>free lattices</term>
<term>logique linéaire</term>
<term>problème de décision</term>
<term>sequent calculus</term>
<term>treillis libre</term>
</keywords>
</textClass>
<langUsage><language ident="en">en</language>
</langUsage>
</profileDesc>
</teiHeader>
<front><div type="abstract" xml:lang="en">Abstract: The additive fragment of linear logic is complete for general (nondistributive) lattices. A sequent calculus for general lattices is presented with multiple antecedents and succedents. This construction is extended to give a sequent calculus for prepositional linear logic with both additive and multiplicative contexts. Then, various decision procedures are investigated for general lattices.</div>
</front>
</TEI>
<double idat="0304-3975:1999:Marion J:from:multiple:sequent"><HAL><TEI><teiHeader><fileDesc><titleStmt><title xml:lang="en">From multiple sequent for Additive Linear Logic to decision procedures for Free Lattices</title>
<author><name sortKey="Marion, Jean Yves" sort="Marion, Jean Yves" uniqKey="Marion J" first="Jean-Yves" last="Marion">Jean-Yves Marion</name>
<affiliation wicri:level="1"><hal:affiliation type="researchteam" xml:id="struct-2347" status="OLD"><idno type="RNSR">199618306V</idno>
<orgName>Linear logic, proof networks and categorial grammars</orgName>
<orgName type="acronym">CALLIGRAMME</orgName>
<desc><address><country key="FR"></country>
</address>
<ref type="url">http://www.inria.fr/equipes/calligramme</ref>
</desc>
<listRelation><relation active="#struct-160" type="direct"></relation>
<relation name="UMR7503" active="#struct-441569" type="indirect"></relation>
<relation active="#struct-300009" type="indirect"></relation>
<relation active="#struct-300291" type="indirect"></relation>
<relation active="#struct-300292" type="indirect"></relation>
<relation active="#struct-300293" type="indirect"></relation>
<relation active="#struct-2496" type="direct"></relation>
</listRelation>
<tutelles><tutelle active="#struct-160" type="direct"><org type="laboratory" xml:id="struct-160" status="OLD"><orgName>Laboratoire Lorrain de Recherche en Informatique et ses Applications</orgName>
<orgName type="acronym">LORIA</orgName>
<desc><address><addrLine>Campus Scientifique BP 239 54506 Vandoeuvre-lès-Nancy Cedex</addrLine>
<country key="FR"></country>
</address>
<ref type="url">http://www.loria.fr</ref>
</desc>
<listRelation><relation name="UMR7503" active="#struct-441569" type="direct"></relation>
<relation active="#struct-300009" type="direct"></relation>
<relation active="#struct-300291" type="direct"></relation>
<relation active="#struct-300292" type="direct"></relation>
<relation active="#struct-300293" type="direct"></relation>
</listRelation>
</org>
</tutelle>
<tutelle name="UMR7503" active="#struct-441569" type="indirect"><org type="institution" xml:id="struct-441569" status="VALID"><idno type="ISNI">0000000122597504</idno>
<idno type="IdRef">02636817X</idno>
<orgName>Centre National de la Recherche Scientifique</orgName>
<orgName type="acronym">CNRS</orgName>
<date type="start">1939-10-19</date>
<desc><address><country key="FR"></country>
</address>
<ref type="url">http://www.cnrs.fr/</ref>
</desc>
</org>
</tutelle>
<tutelle active="#struct-300009" type="indirect"><org type="institution" xml:id="struct-300009" status="VALID"><orgName>Institut National de Recherche en Informatique et en Automatique</orgName>
<orgName type="acronym">Inria</orgName>
<desc><address><addrLine>Domaine de VoluceauRocquencourt - BP 10578153 Le Chesnay Cedex</addrLine>
<country key="FR"></country>
</address>
<ref type="url">http://www.inria.fr/en/</ref>
</desc>
</org>
</tutelle>
<tutelle active="#struct-300291" type="indirect"><org type="institution" xml:id="struct-300291" status="OLD"><orgName>Université Henri Poincaré - Nancy 1</orgName>
<orgName type="acronym">UHP</orgName>
<date type="end">2011-12-31</date>
<desc><address><addrLine>24-30 rue Lionnois, BP 60120, 54 003 NANCY cedex, France</addrLine>
<country key="FR"></country>
</address>
</desc>
</org>
</tutelle>
<tutelle active="#struct-300292" type="indirect"><org type="institution" xml:id="struct-300292" status="OLD"><orgName>Université Nancy 2</orgName>
<date type="end">2011-12-31</date>
<desc><address><addrLine>91 avenue de la Libération, BP 454, 54001 Nancy cedex</addrLine>
<country key="FR"></country>
</address>
</desc>
</org>
</tutelle>
<tutelle active="#struct-300293" type="indirect"><org type="institution" xml:id="struct-300293" status="OLD"><orgName>Institut National Polytechnique de Lorraine</orgName>
<orgName type="acronym">INPL</orgName>
<date type="end">2011-12-31</date>
<desc><address><country key="FR"></country>
</address>
</desc>
</org>
</tutelle>
<tutelle active="#struct-2496" type="direct"><org type="laboratory" xml:id="struct-2496" status="OLD"><orgName>INRIA Lorraine</orgName>
<desc><address><addrLine>615 rue du Jardin Botanique 54600 Villers-lès-Nancy</addrLine>
<country key="FR"></country>
</address>
<ref type="url">http://www.inria.fr/centre-de-recherche-inria/nancy-grand-est</ref>
</desc>
<listRelation><relation active="#struct-300009" type="direct"></relation>
</listRelation>
</org>
</tutelle>
</tutelles>
</hal:affiliation>
<country>France</country>
<placeName><settlement type="city">Nancy</settlement>
<region type="region" nuts="2">Grand Est</region>
<region type="old region" nuts="2">Lorraine (région)</region>
</placeName>
<orgName type="university">Université Nancy 2</orgName>
<orgName type="institution" wicri:auto="newGroup">Université de Lorraine</orgName>
<placeName><settlement type="city">Nancy</settlement>
<region type="region" nuts="2">Grand Est</region>
<region type="old region" nuts="2">Lorraine (région)</region>
</placeName>
<orgName type="university">Institut national polytechnique de Lorraine</orgName>
<orgName type="institution" wicri:auto="newGroup">Université de Lorraine</orgName>
</affiliation>
</author>
</titleStmt>
<publicationStmt><idno type="wicri:source">HAL</idno>
<idno type="RBID">Hal:inria-00098803</idno>
<idno type="halId">inria-00098803</idno>
<idno type="halUri">https://hal.inria.fr/inria-00098803</idno>
<idno type="url">https://hal.inria.fr/inria-00098803</idno>
<date when="1999">1999</date>
<idno type="wicri:Area/Hal/Corpus">002492</idno>
<idno type="wicri:Area/Hal/Curation">002492</idno>
<idno type="wicri:Area/Hal/Checkpoint">006652</idno>
<idno type="wicri:explorRef" wicri:stream="Hal" wicri:step="Checkpoint">006652</idno>
<idno type="wicri:doubleKey">0304-3975:1999:Marion J:from:multiple:sequent</idno>
<idno type="wicri:Area/Main/Merge">00B431</idno>
</publicationStmt>
<sourceDesc><biblStruct><analytic><title xml:lang="en">From multiple sequent for Additive Linear Logic to decision procedures for Free Lattices</title>
<author><name sortKey="Marion, Jean Yves" sort="Marion, Jean Yves" uniqKey="Marion J" first="Jean-Yves" last="Marion">Jean-Yves Marion</name>
<affiliation wicri:level="1"><hal:affiliation type="researchteam" xml:id="struct-2347" status="OLD"><idno type="RNSR">199618306V</idno>
<orgName>Linear logic, proof networks and categorial grammars</orgName>
<orgName type="acronym">CALLIGRAMME</orgName>
<desc><address><country key="FR"></country>
</address>
<ref type="url">http://www.inria.fr/equipes/calligramme</ref>
</desc>
<listRelation><relation active="#struct-160" type="direct"></relation>
<relation name="UMR7503" active="#struct-441569" type="indirect"></relation>
<relation active="#struct-300009" type="indirect"></relation>
<relation active="#struct-300291" type="indirect"></relation>
<relation active="#struct-300292" type="indirect"></relation>
<relation active="#struct-300293" type="indirect"></relation>
<relation active="#struct-2496" type="direct"></relation>
</listRelation>
<tutelles><tutelle active="#struct-160" type="direct"><org type="laboratory" xml:id="struct-160" status="OLD"><orgName>Laboratoire Lorrain de Recherche en Informatique et ses Applications</orgName>
<orgName type="acronym">LORIA</orgName>
<desc><address><addrLine>Campus Scientifique BP 239 54506 Vandoeuvre-lès-Nancy Cedex</addrLine>
<country key="FR"></country>
</address>
<ref type="url">http://www.loria.fr</ref>
</desc>
<listRelation><relation name="UMR7503" active="#struct-441569" type="direct"></relation>
<relation active="#struct-300009" type="direct"></relation>
<relation active="#struct-300291" type="direct"></relation>
<relation active="#struct-300292" type="direct"></relation>
<relation active="#struct-300293" type="direct"></relation>
</listRelation>
</org>
</tutelle>
<tutelle name="UMR7503" active="#struct-441569" type="indirect"><org type="institution" xml:id="struct-441569" status="VALID"><idno type="ISNI">0000000122597504</idno>
<idno type="IdRef">02636817X</idno>
<orgName>Centre National de la Recherche Scientifique</orgName>
<orgName type="acronym">CNRS</orgName>
<date type="start">1939-10-19</date>
<desc><address><country key="FR"></country>
</address>
<ref type="url">http://www.cnrs.fr/</ref>
</desc>
</org>
</tutelle>
<tutelle active="#struct-300009" type="indirect"><org type="institution" xml:id="struct-300009" status="VALID"><orgName>Institut National de Recherche en Informatique et en Automatique</orgName>
<orgName type="acronym">Inria</orgName>
<desc><address><addrLine>Domaine de VoluceauRocquencourt - BP 10578153 Le Chesnay Cedex</addrLine>
<country key="FR"></country>
</address>
<ref type="url">http://www.inria.fr/en/</ref>
</desc>
</org>
</tutelle>
<tutelle active="#struct-300291" type="indirect"><org type="institution" xml:id="struct-300291" status="OLD"><orgName>Université Henri Poincaré - Nancy 1</orgName>
<orgName type="acronym">UHP</orgName>
<date type="end">2011-12-31</date>
<desc><address><addrLine>24-30 rue Lionnois, BP 60120, 54 003 NANCY cedex, France</addrLine>
<country key="FR"></country>
</address>
</desc>
</org>
</tutelle>
<tutelle active="#struct-300292" type="indirect"><org type="institution" xml:id="struct-300292" status="OLD"><orgName>Université Nancy 2</orgName>
<date type="end">2011-12-31</date>
<desc><address><addrLine>91 avenue de la Libération, BP 454, 54001 Nancy cedex</addrLine>
<country key="FR"></country>
</address>
</desc>
</org>
</tutelle>
<tutelle active="#struct-300293" type="indirect"><org type="institution" xml:id="struct-300293" status="OLD"><orgName>Institut National Polytechnique de Lorraine</orgName>
<orgName type="acronym">INPL</orgName>
<date type="end">2011-12-31</date>
<desc><address><country key="FR"></country>
</address>
</desc>
</org>
</tutelle>
<tutelle active="#struct-2496" type="direct"><org type="laboratory" xml:id="struct-2496" status="OLD"><orgName>INRIA Lorraine</orgName>
<desc><address><addrLine>615 rue du Jardin Botanique 54600 Villers-lès-Nancy</addrLine>
<country key="FR"></country>
</address>
<ref type="url">http://www.inria.fr/centre-de-recherche-inria/nancy-grand-est</ref>
</desc>
<listRelation><relation active="#struct-300009" type="direct"></relation>
</listRelation>
</org>
</tutelle>
</tutelles>
</hal:affiliation>
<country>France</country>
<placeName><settlement type="city">Nancy</settlement>
<region type="region" nuts="2">Grand Est</region>
<region type="old region" nuts="2">Lorraine (région)</region>
</placeName>
<orgName type="university">Université Nancy 2</orgName>
<orgName type="institution" wicri:auto="newGroup">Université de Lorraine</orgName>
<placeName><settlement type="city">Nancy</settlement>
<region type="region" nuts="2">Grand Est</region>
<region type="old region" nuts="2">Lorraine (région)</region>
</placeName>
<orgName type="university">Institut national polytechnique de Lorraine</orgName>
<orgName type="institution" wicri:auto="newGroup">Université de Lorraine</orgName>
</affiliation>
</author>
</analytic>
<series><title level="j">Theoretical Computer Science</title>
<idno type="ISSN">0304-3975</idno>
<imprint><date type="datePub">1999</date>
</imprint>
</series>
</biblStruct>
</sourceDesc>
</fileDesc>
<profileDesc><textClass><keywords scheme="mix" xml:lang="fr"><term>additive linear logic</term>
<term>calcul des séquents</term>
<term>decision procedure</term>
<term>fragment additif</term>
<term>free lattices</term>
<term>logique linéaire</term>
<term>problème de décision</term>
<term>sequent calculus</term>
<term>treillis libre</term>
</keywords>
</textClass>
</profileDesc>
</teiHeader>
<front><div type="abstract" xml:lang="en">The additive fragment of linear logic is complete for general (non-distributive) lattices. A sequent calculus for general lattices is presented with multiple antecedents and succedents. This construction is extended to give a sequent calculus for propositional linear logic with both additive and multiplicative contexts. Then, various decision procedures are investigated for general lattices.</div>
</front>
</TEI>
</HAL>
<INIST><TEI><teiHeader><fileDesc><titleStmt><title xml:lang="en" level="a">From multiple sequent for additive linear logic to decision procedures for free lattices</title>
<author><name sortKey="Marion, J Y" sort="Marion, J Y" uniqKey="Marion J" first="J.-Y." last="Marion">J.-Y. Marion</name>
<affiliation wicri:level="4"><inist:fA14 i1="01"><s1>Universitè Nancy 2, Loria, Projet Calligramme, Campus Scientifique - B.P. 239</s1>
<s2>54506 Vandoeuvre-lès-Nancy</s2>
<s3>FRA</s3>
<sZ>1 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é Nancy 2</orgName>
</affiliation>
</author>
</titleStmt>
<publicationStmt><idno type="wicri:source">INIST</idno>
<idno type="inist">99-0463969</idno>
<date when="1999">1999</date>
<idno type="stanalyst">PASCAL 99-0463969 INIST</idno>
<idno type="RBID">Pascal:99-0463969</idno>
<idno type="wicri:Area/PascalFrancis/Corpus">000B00</idno>
<idno type="wicri:Area/PascalFrancis/Curation">000D70</idno>
<idno type="wicri:Area/PascalFrancis/Checkpoint">000A83</idno>
<idno type="wicri:explorRef" wicri:stream="PascalFrancis" wicri:step="Checkpoint">000A83</idno>
<idno type="wicri:doubleKey">0304-3975:1999:Marion J:from:multiple:sequent</idno>
<idno type="wicri:Area/Main/Merge">00B171</idno>
</publicationStmt>
<sourceDesc><biblStruct><analytic><title xml:lang="en" level="a">From multiple sequent for additive linear logic to decision procedures for free lattices</title>
<author><name sortKey="Marion, J Y" sort="Marion, J Y" uniqKey="Marion J" first="J.-Y." last="Marion">J.-Y. Marion</name>
<affiliation wicri:level="4"><inist:fA14 i1="01"><s1>Universitè Nancy 2, Loria, Projet Calligramme, Campus Scientifique - B.P. 239</s1>
<s2>54506 Vandoeuvre-lès-Nancy</s2>
<s3>FRA</s3>
<sZ>1 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é Nancy 2</orgName>
</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="1999">1999</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>Computational complexity</term>
<term>Decision theory</term>
<term>Lattice</term>
<term>Mathematical logic</term>
<term>Propositional calculus</term>
<term>Propositional logic</term>
</keywords>
<keywords scheme="Pascal" xml:lang="fr"><term>Complexité calcul</term>
<term>Logique mathématique</term>
<term>Calcul propositionnel</term>
<term>Logique propositionnelle</term>
<term>Treillis</term>
<term>Théorie décision</term>
</keywords>
</textClass>
</profileDesc>
</teiHeader>
<front><div type="abstract" xml:lang="en">The additive fragment of linear logic is complete for general (nondistributive) lattices. A sequent calculus for general lattices is presented with multiple antecedents and succedents. This construction is extended to give a sequent calculus for propositional linear logic with both additive and multiplicative contexts. Then, various decision procedures are investigated for general lattices.</div>
</front>
</TEI>
</INIST>
<ISTEX><TEI wicri:istexFullTextTei="biblStruct"><teiHeader><fileDesc><titleStmt><title>From multiple sequent for additive linear logic to decision procedures for free lattices</title>
<author><name sortKey="Marion, Jean Yves" sort="Marion, Jean Yves" uniqKey="Marion J" first="Jean-Yves" last="Marion">Jean-Yves Marion</name>
</author>
</titleStmt>
<publicationStmt><idno type="wicri:source">ISTEX</idno>
<idno type="RBID">ISTEX:8085993A8FC74D69CBBC4756251EBEE223170CB4</idno>
<date when="1999" year="1999">1999</date>
<idno type="doi">10.1016/S0304-3975(98)00311-9</idno>
<idno type="url">https://api.istex.fr/ark:/67375/6H6-N5RQFN93-0/fulltext.pdf</idno>
<idno type="wicri:Area/Istex/Corpus">001D83</idno>
<idno type="wicri:explorRef" wicri:stream="Istex" wicri:step="Corpus" wicri:corpus="ISTEX">001D83</idno>
<idno type="wicri:Area/Istex/Curation">001D60</idno>
<idno type="wicri:Area/Istex/Checkpoint">002229</idno>
<idno type="wicri:explorRef" wicri:stream="Istex" wicri:step="Checkpoint">002229</idno>
<idno type="wicri:doubleKey">0304-3975:1999:Marion J:from:multiple:sequent</idno>
<idno type="wicri:Area/Main/Merge">00AE96</idno>
</publicationStmt>
<sourceDesc><biblStruct><analytic><title level="a">From multiple sequent for additive linear logic to decision procedures for free lattices</title>
<author><name sortKey="Marion, Jean Yves" sort="Marion, Jean Yves" uniqKey="Marion J" first="Jean-Yves" last="Marion">Jean-Yves Marion</name>
<affiliation wicri:level="4"><country xml:lang="fr">France</country>
<wicri:regionArea>Université Nancy 2, Loria, Projet Calligramme, Campus Scientifique — B.P. 239, 54506 Vandoeuvre-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é Nancy 2</orgName>
</affiliation>
<affiliation wicri:level="1"><country wicri:rule="url">France</country>
</affiliation>
</author>
</analytic>
<monogr></monogr>
<series><title level="j">Theoretical Computer Science</title>
<title level="j" type="abbrev">TCS</title>
<idno type="ISSN">0304-3975</idno>
<imprint><publisher>ELSEVIER</publisher>
<date type="published" when="1999">1999</date>
<biblScope unit="volume">224</biblScope>
<biblScope unit="issue">1–2</biblScope>
<biblScope unit="page" from="157">157</biblScope>
<biblScope unit="page" to="172">172</biblScope>
</imprint>
<idno type="ISSN">0304-3975</idno>
</series>
</biblStruct>
</sourceDesc>
<seriesStmt><idno type="ISSN">0304-3975</idno>
</seriesStmt>
</fileDesc>
<profileDesc><textClass><keywords scheme="Teeft" xml:lang="en"><term>Additive</term>
<term>Additive context</term>
<term>Additive contexts</term>
<term>Additive fragment</term>
<term>Additive implication</term>
<term>Algorithm</term>
<term>Calculus</term>
<term>Classical propositional logic</term>
<term>Computer science</term>
<term>Connector</term>
<term>Decision procedure</term>
<term>Decision procedures</term>
<term>Distributive lattices</term>
<term>Elsevier science</term>
<term>Free lattice</term>
<term>Free lattices</term>
<term>Free proof</term>
<term>General lattices</term>
<term>Intuitionistic</term>
<term>Last rule</term>
<term>Lattice</term>
<term>Lattice theory</term>
<term>Least element</term>
<term>Lecture notes</term>
<term>Linear logic</term>
<term>Mall</term>
<term>Multiple antecedents</term>
<term>Multiple calculus</term>
<term>Multiple sequent</term>
<term>Multiplicative</term>
<term>Multiplicative contexts</term>
<term>Other hand</term>
<term>Polynomial time</term>
<term>Propositional</term>
<term>Right rule</term>
<term>Right rules</term>
<term>Right side</term>
<term>Same atom</term>
<term>Search space</term>
<term>Seminal work</term>
<term>Sequent</term>
<term>Sequent calculus</term>
<term>Single formula</term>
<term>Structural rules</term>
<term>Theoretical computer science</term>
</keywords>
</textClass>
<langUsage><language ident="en">en</language>
</langUsage>
</profileDesc>
</teiHeader>
<front><div type="abstract" xml:lang="en">Abstract: The additive fragment of linear logic is complete for general (nondistributive) lattices. A sequent calculus for general lattices is presented with multiple antecedents and succedents. This construction is extended to give a sequent calculus for prepositional linear logic with both additive and multiplicative contexts. Then, various decision procedures are investigated for general lattices.</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 00A844 | SxmlIndent | more

HfdSelect -h $EXPLOR_AREA/Data/Main/Curation/biblio.hfd -nk 00A844 | 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:8085993A8FC74D69CBBC4756251EBEE223170CB4
   |texte=   From multiple sequent for additive linear logic to decision procedures for free lattices
}}

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

From multiple sequent for additive linear logic to decision procedures for free lattices

From multiple sequent for additive linear logic to decision procedures for free lattices

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