Proof-search and Proof Nets in Mixed Linear Logic
Identifieur interne : 001F71 ( Istex/Checkpoint ); précédent : 001F70; suivant : 001F72Proof-search and Proof Nets in Mixed Linear Logic
Auteurs : D. Galmiche [France] ; J. M. Notin [France]Source :
- Electronic Notes in Theoretical Computer Science [ 1571-0661 ] ; 2000.
English descriptors
- Teeft :
- Algorithm, Automatic proof nets construction, Calculus, Commutative, Commutative connectives, Computer science, Concurrent constraint programming, Connective, Constraint, Constraints satisfaction, Decomposition tree, Downward rules, Dual literals, Electronic notes, Elementary proof nets, Extension rule, Extension rules, Free switchings, Galmiche, Gure, Initial sequent, Inner part, Inner parts, Label, Label moves, Label propagation, Labels travel, Linear logic, Link crossings, Links, Mmll, Mmll proof, Mmll proof structure, Mmll sequent, Mmll sequent calculus, Multiplicative, Multiplicative fragment, Ncmll, Ncmll proof, Node, Notin, Order constraints, Other cases, Partial proof, Previous example, Proof nets, Proof nets construction, Proof structure, Proof structures, Proof systems, Propagation rules, Provability, Provable, Resp, Right premise, Search process, Sequent, Sequent calculus, Static labels, Subnets, Theoretical computer science, Unique cycle, Various links.
Abstract
Abstract: In this paper we study how to design proof-search methods for the multiplicative fragment of Mixed Linear Logic which combines both commutative and noncommutative connectives. After an analysis of the interaction and relationships between these connectives, we propose two different proof-search algorithms, both based on the construction of labelled proof nets. The labels allow in the former to fix some constraints to satisfy during the proof net search and in the latter to propagate some informations useful to guide and control the search. Such based-on proof nets methods are useful to efficiently detect the non-provability and could lead to the generation of some countermodels.
Url:
DOI: 10.1016/S1571-0661(05)01137-0
Affiliations:
Links toward previous steps (curation, corpus...)
Links to Exploration step
ISTEX:CA7C9DAF8DC2E3BD0EAEBA852CD7E3349FE3BFCCLe document en format XML
<record><TEI wicri:istexFullTextTei="biblStruct"><teiHeader><fileDesc><titleStmt><title>Proof-search and Proof Nets in Mixed Linear 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:CA7C9DAF8DC2E3BD0EAEBA852CD7E3349FE3BFCC</idno><date when="2000" year="2000">2000</date><idno type="doi">10.1016/S1571-0661(05)01137-0</idno><idno type="url">https://api.istex.fr/ark:/67375/6H6-V3TR7Q40-H/fulltext.pdf</idno><idno type="wicri:Area/Istex/Corpus">003003</idno><idno type="wicri:explorRef" wicri:stream="Istex" wicri:step="Corpus" wicri:corpus="ISTEX">003003</idno><idno type="wicri:Area/Istex/Curation">002F64</idno><idno type="wicri:Area/Istex/Checkpoint">001F71</idno><idno type="wicri:explorRef" wicri:stream="Istex" wicri:step="Checkpoint">001F71</idno></publicationStmt><sourceDesc><biblStruct><analytic><title level="a">Proof-search and Proof Nets in Mixed Linear Logic</title><author><name sortKey="Galmiche, D" sort="Galmiche, D" uniqKey="Galmiche D" first="D." last="Galmiche">D. Galmiche</name><affiliation wicri:level="1"><country xml:lang="fr">France</country><wicri:regionArea>LORIA UMR 7503 UHP Nancy 1 Campus Scientifique, BP 239 Vanduvre-ls-Nancy</wicri:regionArea><wicri:noRegion>BP 239 Vanduvre-ls-Nancy</wicri:noRegion><wicri:noRegion>BP 239 Vanduvre-ls-Nancy</wicri:noRegion></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="1"><country xml:lang="fr">France</country><wicri:regionArea>LORIA UMR 7503 UHP Nancy 1 Campus Scientifique, BP 239 Vanduvre-ls-Nancy</wicri:regionArea><wicri:noRegion>BP 239 Vanduvre-ls-Nancy</wicri:noRegion><wicri:noRegion>BP 239 Vanduvre-ls-Nancy</wicri:noRegion></affiliation><affiliation wicri:level="1"><country wicri:rule="url">France</country></affiliation></author></analytic><monogr></monogr><series><title level="j">Electronic Notes in Theoretical Computer Science</title><title level="j" type="abbrev">ENTCS</title><idno type="ISSN">1571-0661</idno><imprint><publisher>ELSEVIER</publisher><date type="published" when="2000">2000</date><biblScope unit="volume">37</biblScope><biblScope unit="supplement">C</biblScope><biblScope unit="page" from="1">1</biblScope><biblScope unit="page" to="33">33</biblScope></imprint><idno type="ISSN">1571-0661</idno></series></biblStruct></sourceDesc><seriesStmt><idno type="ISSN">1571-0661</idno></seriesStmt></fileDesc><profileDesc><textClass><keywords scheme="Teeft" xml:lang="en"><term>Algorithm</term><term>Automatic proof nets construction</term><term>Calculus</term><term>Commutative</term><term>Commutative connectives</term><term>Computer science</term><term>Concurrent constraint programming</term><term>Connective</term><term>Constraint</term><term>Constraints satisfaction</term><term>Decomposition tree</term><term>Downward rules</term><term>Dual literals</term><term>Electronic notes</term><term>Elementary proof nets</term><term>Extension rule</term><term>Extension rules</term><term>Free switchings</term><term>Galmiche</term><term>Gure</term><term>Initial sequent</term><term>Inner part</term><term>Inner parts</term><term>Label</term><term>Label moves</term><term>Label propagation</term><term>Labels travel</term><term>Linear logic</term><term>Link crossings</term><term>Links</term><term>Mmll</term><term>Mmll proof</term><term>Mmll proof structure</term><term>Mmll sequent</term><term>Mmll sequent calculus</term><term>Multiplicative</term><term>Multiplicative fragment</term><term>Ncmll</term><term>Ncmll proof</term><term>Node</term><term>Notin</term><term>Order constraints</term><term>Other cases</term><term>Partial proof</term><term>Previous example</term><term>Proof nets</term><term>Proof nets construction</term><term>Proof structure</term><term>Proof structures</term><term>Proof systems</term><term>Propagation rules</term><term>Provability</term><term>Provable</term><term>Resp</term><term>Right premise</term><term>Search process</term><term>Sequent</term><term>Sequent calculus</term><term>Static labels</term><term>Subnets</term><term>Theoretical computer science</term><term>Unique cycle</term><term>Various links</term></keywords></textClass><langUsage><language ident="en">en</language></langUsage></profileDesc></teiHeader><front><div type="abstract" xml:lang="en">Abstract: In this paper we study how to design proof-search methods for the multiplicative fragment of Mixed Linear Logic which combines both commutative and noncommutative connectives. After an analysis of the interaction and relationships between these connectives, we propose two different proof-search algorithms, both based on the construction of labelled proof nets. The labels allow in the former to fix some constraints to satisfy during the proof net search and in the latter to propagate some informations useful to guide and control the search. Such based-on proof nets methods are useful to efficiently detect the non-provability and could lead to the generation of some countermodels.</div></front></TEI><affiliations><list><country><li>France</li></country></list><tree><country name="France"><noRegion><name sortKey="Galmiche, D" sort="Galmiche, D" uniqKey="Galmiche D" first="D." last="Galmiche">D. Galmiche</name></noRegion><name sortKey="Galmiche, D" sort="Galmiche, D" uniqKey="Galmiche D" first="D." last="Galmiche">D. Galmiche</name><name sortKey="Notin, J M" sort="Notin, J M" uniqKey="Notin J" first="J. M." last="Notin">J. M. Notin</name><name sortKey="Notin, J M" sort="Notin, J M" uniqKey="Notin J" first="J. M." last="Notin">J. M. Notin</name></country></tree></affiliations></record>Pour manipuler ce document sous Unix (Dilib)
EXPLOR_STEP=$WICRI_ROOT/Wicri/Lorraine/explor/InforLorV4/Data/Istex/Checkpoint
HfdSelect -h $EXPLOR_STEP/biblio.hfd -nk 001F71 | SxmlIndent | more
Ou
HfdSelect -h $EXPLOR_AREA/Data/Istex/Checkpoint/biblio.hfd -nk 001F71 | SxmlIndent | more
Pour mettre un lien sur cette page dans le réseau Wicri
{{Explor lien
|wiki= Wicri/Lorraine
|area= InforLorV4
|flux= Istex
|étape= Checkpoint
|type= RBID
|clé= ISTEX:CA7C9DAF8DC2E3BD0EAEBA852CD7E3349FE3BFCC
|texte= Proof-search and Proof Nets in Mixed Linear Logic
}}
| This area was generated with Dilib version V0.6.33. |  |