From multiple sequent for additive linear logic to decision procedures for free lattices
Identifieur interne : 00A844 ( Main/Exploration ); précédent : 00A843; suivant : 00A845From multiple sequent for additive linear logic to decision procedures for free lattices
Auteurs : Jean-Yves Marion [France]Source :
- Theoretical Computer Science [ 0304-3975 ] ; 1999.
Descripteurs français
- Pascal (Inist)
- mix :
English descriptors
- KwdEn :
- 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
Affiliations:
Links toward previous steps (curation, corpus...)
- to stream Istex, to step Corpus: 001D83
- to stream Istex, to step Curation: 001D60
- to stream Istex, to step Checkpoint: 002229
- to stream Main, to step Merge: 00AE96
- to stream Hal, to step Corpus: 002492
- to stream Hal, to step Curation: 002492
- to stream Hal, to step Checkpoint: 006652
- to stream Main, to step Merge: 00B431
- to stream PascalFrancis, to step Corpus: 000B00
- to stream PascalFrancis, to step Curation: 000D70
- to stream PascalFrancis, to step Checkpoint: 000A83
- to stream Main, to step Merge: 00B171
- to stream Main, to step Curation: 00A844
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><idno type="wicri:Area/Main/Exploration">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><affiliations><list><country><li>France</li></country><region><li>Grand Est</li><li>Lorraine (région)</li></region><settlement><li>Vandœuvre-lès-Nancy</li></settlement><orgName><li>Université Nancy 2</li></orgName></list><tree><country name="France"><region name="Grand Est"><name sortKey="Marion, Jean Yves" sort="Marion, Jean Yves" uniqKey="Marion J" first="Jean-Yves" last="Marion">Jean-Yves Marion</name></region><name sortKey="Marion, Jean Yves" sort="Marion, Jean Yves" uniqKey="Marion J" first="Jean-Yves" last="Marion">Jean-Yves Marion</name></country></tree></affiliations></record>Pour manipuler ce document sous Unix (Dilib)
EXPLOR_STEP=$WICRI_ROOT/Wicri/Lorraine/explor/InforLorV4/Data/Main/Exploration
HfdSelect -h $EXPLOR_STEP/biblio.hfd -nk 00A844 | SxmlIndent | more
Ou
HfdSelect -h $EXPLOR_AREA/Data/Main/Exploration/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= Exploration
|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. |  |