From multiple sequent for additive linear logic to decision procedures for free lattices
Identifieur interne : 001D83 ( Istex/Corpus ); précédent : 001D82; suivant : 001D84From multiple sequent for additive linear logic to decision procedures for free lattices
Auteurs : Jean-Yves MarionSource :
- Theoretical Computer Science [ 0304-3975 ] ; 1999.
English descriptors
- Teeft :
- Additive, Additive context, Additive contexts, Additive fragment, Additive implication, Algorithm, Calculus, Classical propositional logic, Computer science, Connector, Decision procedure, Decision procedures, Distributive lattices, Elsevier science, Free lattice, Free lattices, Free proof, General lattices, Intuitionistic, Last rule, Lattice, Lattice theory, Least element, Lecture notes, Linear logic, Mall, Multiple antecedents, Multiple calculus, Multiple sequent, Multiplicative, Multiplicative contexts, Other hand, Polynomial time, Propositional, Right rule, Right rules, Right side, Same atom, Search space, Seminal work, Sequent, Sequent calculus, Single formula, Structural rules, Theoretical computer science.
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 to Exploration step
ISTEX:8085993A8FC74D69CBBC4756251EBEE223170CB4Le 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><affiliation><mods:affiliation>Université Nancy 2, Loria, Projet Calligramme, Campus Scientifique — B.P. 239, 54506 Vandoeuvre-lès-Nancy Cedex, France</mods:affiliation></affiliation><affiliation><mods:affiliation>E-mail: jean-yves.marion@loria.fr</mods:affiliation></affiliation></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></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><mods:affiliation>Université Nancy 2, Loria, Projet Calligramme, Campus Scientifique — B.P. 239, 54506 Vandoeuvre-lès-Nancy Cedex, France</mods:affiliation></affiliation><affiliation><mods:affiliation>E-mail: jean-yves.marion@loria.fr</mods:affiliation></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><corpusName>elsevier</corpusName><keywords><teeft><json:string>calculus</json:string><json:string>sequent</json:string><json:string>linear logic</json:string><json:string>sequent calculus</json:string><json:string>computer science</json:string><json:string>propositional</json:string><json:string>lattice</json:string><json:string>last rule</json:string><json:string>structural rules</json:string><json:string>intuitionistic</json:string><json:string>free lattices</json:string><json:string>multiplicative</json:string><json:string>connector</json:string><json:string>additive contexts</json:string><json:string>theoretical computer science</json:string><json:string>additive</json:string><json:string>free lattice</json:string><json:string>algorithm</json:string><json:string>right rules</json:string><json:string>decision procedure</json:string><json:string>free proof</json:string><json:string>general lattices</json:string><json:string>mall</json:string><json:string>additive context</json:string><json:string>multiplicative contexts</json:string><json:string>distributive lattices</json:string><json:string>least element</json:string><json:string>additive fragment</json:string><json:string>decision procedures</json:string><json:string>right side</json:string><json:string>other hand</json:string><json:string>seminal work</json:string><json:string>multiple calculus</json:string><json:string>multiple antecedents</json:string><json:string>single formula</json:string><json:string>additive implication</json:string><json:string>multiple sequent</json:string><json:string>elsevier science</json:string><json:string>search space</json:string><json:string>classical propositional logic</json:string><json:string>polynomial time</json:string><json:string>same atom</json:string><json:string>right rule</json:string><json:string>lattice theory</json:string><json:string>lecture notes</json:string></teeft></keywords><author><json:item><name>Jean-Yves Marion</name><affiliations><json:string>Université Nancy 2, Loria, Projet Calligramme, Campus Scientifique — B.P. 239, 54506 Vandoeuvre-lès-Nancy Cedex, France</json:string><json:string>E-mail: jean-yves.marion@loria.fr</json:string></affiliations></json:item></author><subject><json:item><lang><json:string>eng</json:string></lang><value>Free lattices</value></json:item><json:item><lang><json:string>eng</json:string></lang><value>Additive linear logic</value></json:item><json:item><lang><json:string>eng</json:string></lang><value>Sequent calculus</value></json:item><json:item><lang><json:string>eng</json:string></lang><value>Decision procedure</value></json:item></subject><arkIstex>ark:/67375/6H6-N5RQFN93-0</arkIstex><language><json:string>eng</json:string></language><originalGenre><json:string>Full-length article</json:string></originalGenre><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.</abstract><qualityIndicators><score>6.534</score><pdfWordCount>3886</pdfWordCount><pdfCharCount>22589</pdfCharCount><pdfVersion>1.2</pdfVersion><pdfPageCount>16</pdfPageCount><pdfPageSize>468 x 684 pts</pdfPageSize><refBibsNative>true</refBibsNative><abstractWordCount>54</abstractWordCount><abstractCharCount>403</abstractCharCount><keywordCount>4</keywordCount></qualityIndicators><title>From multiple sequent for additive linear logic to decision procedures for free lattices</title><pii><json:string>S0304-3975(98)00311-9</json:string></pii><genre><json:string>research-article</json:string></genre><serie><title>Ch. III.3</title><language><json:string>unknown</json:string></language><pages><first>117</first><last>224</last></pages></serie><host><title>Theoretical Computer Science</title><language><json:string>unknown</json:string></language><publicationDate>1999</publicationDate><issn><json:string>0304-3975</json:string></issn><pii><json:string>S0304-3975(00)X0117-X</json:string></pii><volume>224</volume><issue>1–2</issue><pages><first>157</first><last>172</last></pages><genre><json:string>journal</json:string></genre></host><namedEntities><unitex><date><json:string>1999</json:string></date><geogName></geogName><orgName></orgName><orgName_funder></orgName_funder><orgName_provider></orgName_provider><persName><json:string>Nancy Cedex</json:string><json:string>Y. Marion</json:string><json:string>A. Inversion</json:string><json:string>Y. Murionl</json:string></persName><placeName></placeName><ref_url></ref_url><ref_bibl><json:string>[12,9,14]</json:string><json:string>[6]</json:string><json:string>[16]</json:string><json:string>[5]</json:string><json:string>[4,8]</json:string><json:string>[2]</json:string></ref_bibl><bibl></bibl></unitex></namedEntities><ark><json:string>ark:/67375/6H6-N5RQFN93-0</json:string></ark><categories><wos><json:string>1 - science</json:string><json:string>2 - computer science, theory & methods</json:string></wos><scienceMetrix><json:string>1 - applied sciences</json:string><json:string>2 - information & communication technologies</json:string><json:string>3 - computation theory & mathematics</json:string></scienceMetrix><scopus><json:string>1 - Physical Sciences</json:string><json:string>2 - Computer Science</json:string><json:string>3 - General Computer Science</json:string><json:string>1 - Physical Sciences</json:string><json:string>2 - Mathematics</json:string><json:string>3 - Theoretical Computer Science</json:string></scopus><inist><json:string>1 - sciences appliquees, technologies et medecines</json:string><json:string>2 - sciences exactes et technologie</json:string><json:string>3 - sciences et techniques communes</json:string><json:string>4 - mathematiques</json:string></inist></categories><publicationDate>1999</publicationDate><copyrightDate>1999</copyrightDate><doi><json:string>10.1016/S0304-3975(98)00311-9</json:string></doi><id>8085993A8FC74D69CBBC4756251EBEE223170CB4</id><score>1</score><fulltext><json:item><extension>pdf</extension><original>true</original><mimetype>application/pdf</mimetype><uri>https://api.istex.fr/ark:/67375/6H6-N5RQFN93-0/fulltext.pdf</uri></json:item><json:item><extension>zip</extension><original>false</original><mimetype>application/zip</mimetype><uri>https://api.istex.fr/ark:/67375/6H6-N5RQFN93-0/bundle.zip</uri></json:item><istex:fulltextTEI uri="https://api.istex.fr/ark:/67375/6H6-N5RQFN93-0/fulltext.tei"><teiHeader><fileDesc><titleStmt><title level="a">From multiple sequent for additive linear logic to decision procedures for free lattices</title></titleStmt><publicationStmt><authority>ISTEX</authority><publisher scheme="https://scientific-publisher.data.istex.fr">ELSEVIER</publisher><availability><licence><p>elsevier</p></licence></availability><p scheme="https://loaded-corpus.data.istex.fr/ark:/67375/XBH-HKKZVM7B-M"></p><date>1999</date></publicationStmt><notesStmt><note type="research-article" scheme="https://content-type.data.istex.fr/ark:/67375/XTP-1JC4F85T-7">research-article</note><note type="journal" scheme="https://publication-type.data.istex.fr/ark:/67375/JMC-0GLKJH51-B">journal</note><note type="content">Section title: Contribution</note></notesStmt><sourceDesc><biblStruct type="inbook"><analytic><title level="a">From multiple sequent for additive linear logic to decision procedures for free lattices</title><author xml:id="author-0000"><persName><forename type="first">Jean-Yves</forename><surname>Marion</surname></persName><email>jean-yves.marion@loria.fr</email><affiliation>Université Nancy 2, Loria, Projet Calligramme, Campus Scientifique — B.P. 239, 54506 Vandoeuvre-lès-Nancy Cedex, France</affiliation></author><idno type="istex">8085993A8FC74D69CBBC4756251EBEE223170CB4</idno><idno type="ark">ark:/67375/6H6-N5RQFN93-0</idno><idno type="DOI">10.1016/S0304-3975(98)00311-9</idno><idno type="PII">S0304-3975(98)00311-9</idno></analytic><monogr><title level="j">Theoretical Computer Science</title><title level="j" type="abbrev">TCS</title><idno type="pISSN">0304-3975</idno><idno type="PII">S0304-3975(00)X0117-X</idno><imprint><publisher>ELSEVIER</publisher><date type="published" when="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></monogr></biblStruct></sourceDesc></fileDesc><profileDesc><creation><date>1999</date></creation><langUsage><language ident="en">en</language></langUsage><abstract xml:lang="en"><p>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.</p></abstract><textClass><keywords scheme="keyword"><list><head>Keywords</head><item><term>Free lattices</term></item><item><term>Additive linear logic</term></item><item><term>Sequent calculus</term></item><item><term>Decision procedure</term></item></list></keywords></textClass></profileDesc><revisionDesc><change when="1999">Published</change></revisionDesc></teiHeader></istex:fulltextTEI><json:item><extension>txt</extension><original>false</original><mimetype>text/plain</mimetype><uri>https://api.istex.fr/ark:/67375/6H6-N5RQFN93-0/fulltext.txt</uri></json:item></fulltext><metadata><istex:metadataXml wicri:clean="Elsevier, elements deleted: tail"><istex:xmlDeclaration>version="1.0" encoding="utf-8"</istex:xmlDeclaration><istex:docType PUBLIC="-//ES//DTD journal article DTD version 4.5.2//EN//XML" URI="art452.dtd" name="istex:docType"></istex:docType><istex:document><converted-article version="4.5.2" docsubtype="fla"><item-info><jid>TCS</jid><aid>98003119</aid><ce:pii>S0304-3975(98)00311-9</ce:pii><ce:doi>10.1016/S0304-3975(98)00311-9</ce:doi><ce:copyright type="unknown" year="1999"></ce:copyright></item-info><head><ce:dochead><ce:textfn>Contribution</ce:textfn></ce:dochead><ce:title>From multiple sequent for additive linear logic to decision procedures for free lattices</ce:title><ce:author-group><ce:author><ce:given-name>Jean-Yves</ce:given-name><ce:surname>Marion</ce:surname><ce:e-address>jean-yves.marion@loria.fr</ce:e-address></ce:author><ce:affiliation><ce:textfn>Université Nancy 2, Loria, Projet Calligramme, Campus Scientifique — B.P. 239, 54506 Vandoeuvre-lès-Nancy Cedex, France</ce:textfn></ce:affiliation></ce:author-group><ce:abstract><ce:section-title>Abstract</ce:section-title><ce:abstract-sec><ce:simple-para>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.</ce:simple-para></ce:abstract-sec></ce:abstract><ce:keywords><ce:section-title>Keywords</ce:section-title><ce:keyword><ce:text>Free lattices</ce:text></ce:keyword><ce:keyword><ce:text>Additive linear logic</ce:text></ce:keyword><ce:keyword><ce:text>Sequent calculus</ce:text></ce:keyword><ce:keyword><ce:text>Decision procedure</ce:text></ce:keyword></ce:keywords></head></converted-article></istex:document></istex:metadataXml><mods version="3.6"><titleInfo><title>From multiple sequent for additive linear logic to decision procedures for free lattices</title></titleInfo><titleInfo type="alternative" contentType="CDATA"><title>From multiple sequent for additive linear logic to decision procedures for free lattices</title></titleInfo><name type="personal"><namePart type="given">Jean-Yves</namePart><namePart type="family">Marion</namePart><affiliation>Université Nancy 2, Loria, Projet Calligramme, Campus Scientifique — B.P. 239, 54506 Vandoeuvre-lès-Nancy Cedex, France</affiliation><affiliation>E-mail: jean-yves.marion@loria.fr</affiliation><role><roleTerm type="text">author</roleTerm></role></name><typeOfResource>text</typeOfResource><genre type="research-article" displayLabel="Full-length article" authority="ISTEX" authorityURI="https://content-type.data.istex.fr" valueURI="https://content-type.data.istex.fr/ark:/67375/XTP-1JC4F85T-7">research-article</genre><originInfo><publisher>ELSEVIER</publisher><dateIssued encoding="w3cdtf">1999</dateIssued><copyrightDate encoding="w3cdtf">1999</copyrightDate></originInfo><language><languageTerm type="code" authority="iso639-2b">eng</languageTerm><languageTerm type="code" authority="rfc3066">en</languageTerm></language><abstract 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.</abstract><note type="content">Section title: Contribution</note><subject><genre>Keywords</genre><topic>Free lattices</topic><topic>Additive linear logic</topic><topic>Sequent calculus</topic><topic>Decision procedure</topic></subject><relatedItem type="host"><titleInfo><title>Theoretical Computer Science</title></titleInfo><titleInfo type="abbreviated"><title>TCS</title></titleInfo><genre type="journal" authority="ISTEX" authorityURI="https://publication-type.data.istex.fr" valueURI="https://publication-type.data.istex.fr/ark:/67375/JMC-0GLKJH51-B">journal</genre><originInfo><publisher>ELSEVIER</publisher><dateIssued encoding="w3cdtf">1999</dateIssued></originInfo><identifier type="ISSN">0304-3975</identifier><identifier type="PII">S0304-3975(00)X0117-X</identifier><part><date>1999</date><detail type="volume"><number>224</number><caption>vol.</caption></detail><detail type="issue"><number>1–2</number><caption>no.</caption></detail><extent unit="issue-pages"><start>1</start><end>353</end></extent><extent unit="pages"><start>157</start><end>172</end></extent></part></relatedItem><identifier type="istex">8085993A8FC74D69CBBC4756251EBEE223170CB4</identifier><identifier type="ark">ark:/67375/6H6-N5RQFN93-0</identifier><identifier type="DOI">10.1016/S0304-3975(98)00311-9</identifier><identifier type="PII">S0304-3975(98)00311-9</identifier><recordInfo><recordContentSource authority="ISTEX" authorityURI="https://loaded-corpus.data.istex.fr" valueURI="https://loaded-corpus.data.istex.fr/ark:/67375/XBH-HKKZVM7B-M">elsevier</recordContentSource></recordInfo></mods><json:item><extension>json</extension><original>false</original><mimetype>application/json</mimetype><uri>https://api.istex.fr/ark:/67375/6H6-N5RQFN93-0/record.json</uri></json:item></metadata></istex></record>Pour manipuler ce document sous Unix (Dilib)
EXPLOR_STEP=$WICRI_ROOT/Wicri/Lorraine/explor/InforLorV4/Data/Istex/Corpus
HfdSelect -h $EXPLOR_STEP/biblio.hfd -nk 001D83 | SxmlIndent | more
Ou
HfdSelect -h $EXPLOR_AREA/Data/Istex/Corpus/biblio.hfd -nk 001D83 | SxmlIndent | more
Pour mettre un lien sur cette page dans le réseau Wicri
{{Explor lien
|wiki= Wicri/Lorraine
|area= InforLorV4
|flux= Istex
|étape= Corpus
|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. |  |