Connection proof search methods in Linear Logic and proof nets construction
Identifieur interne : 006A10 ( Hal/Checkpoint ); précédent : 006A09; suivant : 006A11Connection proof search methods in Linear Logic and proof nets construction
Auteurs : Didier Galmiche [France]Source :
- Theoretical Computer Science [ 0304-3975 ] ; 1998.
Descripteurs français
- mix :
Abstract
In this paper we present proof search methods related with matrix (or connection) characterization of provability for fragments of Linear Logic (LL) and their relationships with automated proof and proof net construction. Non-classical logics as intuitionistic and linear logics are used in various branches of computer science and in many of these applications automated proof methods are needed. In LL the notion of proof net provides a nice, graphical representation of proofs (without some syntactical bureaucracy) and some works emphasized, for instance, the importance of proof nets to analyze evaluation strategies for proof normalization (and thus for computation) taking into account some concurrency and parallelism. We propose here a based on connection characterization of Multiplicative Linear Logic (MLL) and consequently a connection based proof search method that has the nice property to simultaneously construct a proof net (and also a sequent proof) which can be useful within proof environments. From these results, we expect to consider provability and proof nets construction in other LL fragments that are logical foundations of type-theoretic languages.
Url:
Links toward previous steps (curation, corpus...)
Links to Exploration step
Hal:inria-00098601Le document en format XML
<record><TEI><teiHeader><fileDesc><titleStmt><title xml:lang="en">Connection proof search methods in Linear Logic and proof nets construction</title><author><name sortKey="Galmiche, Didier" sort="Galmiche, Didier" uniqKey="Galmiche D" first="Didier" last="Galmiche">Didier Galmiche</name><affiliation wicri:level="1"><hal:affiliation type="researchteam" xml:id="struct-2580" status="OLD"><orgName>Logic, proof Theory and Programming </orgName><orgName type="acronym">TYPES</orgName><desc><address><country key="FR"></country></address><ref type="url">http://www.loria.fr/la-recherche-en/equipes/types</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></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></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-00098601</idno><idno type="halId">inria-00098601</idno><idno type="halUri">https://hal.inria.fr/inria-00098601</idno><idno type="url">https://hal.inria.fr/inria-00098601</idno><date when="1998">1998</date><idno type="wicri:Area/Hal/Corpus">001843</idno><idno type="wicri:Area/Hal/Curation">001843</idno><idno type="wicri:Area/Hal/Checkpoint">006A10</idno><idno type="wicri:explorRef" wicri:stream="Hal" wicri:step="Checkpoint">006A10</idno></publicationStmt><sourceDesc><biblStruct><analytic><title xml:lang="en">Connection proof search methods in Linear Logic and proof nets construction</title><author><name sortKey="Galmiche, Didier" sort="Galmiche, Didier" uniqKey="Galmiche D" first="Didier" last="Galmiche">Didier Galmiche</name><affiliation wicri:level="1"><hal:affiliation type="researchteam" xml:id="struct-2580" status="OLD"><orgName>Logic, proof Theory and Programming </orgName><orgName type="acronym">TYPES</orgName><desc><address><country key="FR"></country></address><ref type="url">http://www.loria.fr/la-recherche-en/equipes/types</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></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></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">1998</date></imprint></series></biblStruct></sourceDesc></fileDesc><profileDesc><textClass><keywords scheme="mix" xml:lang="fr"><term>Automated deduction</term><term>Connection method</term><term>Déduction automatique</term><term>Linear Logic</term><term>Logique Linéaire</term><term>Méthode des connections</term><term>Proof nets</term><term>Réseaux de preuve</term></keywords></textClass></profileDesc></teiHeader><front><div type="abstract" xml:lang="en">In this paper we present proof search methods related with matrix (or connection) characterization of provability for fragments of Linear Logic (LL) and their relationships with automated proof and proof net construction. Non-classical logics as intuitionistic and linear logics are used in various branches of computer science and in many of these applications automated proof methods are needed. In LL the notion of proof net provides a nice, graphical representation of proofs (without some syntactical bureaucracy) and some works emphasized, for instance, the importance of proof nets to analyze evaluation strategies for proof normalization (and thus for computation) taking into account some concurrency and parallelism. We propose here a based on connection characterization of Multiplicative Linear Logic (MLL) and consequently a connection based proof search method that has the nice property to simultaneously construct a proof net (and also a sequent proof) which can be useful within proof environments. From these results, we expect to consider provability and proof nets construction in other LL fragments that are logical foundations of type-theoretic languages.</div></front></TEI><hal api="V3"><titleStmt><title xml:lang="en">Connection proof search methods in Linear Logic and proof nets construction</title><author role="aut"><persName><forename type="first">Didier</forename><surname>Galmiche</surname></persName><email>galmiche@loria.fr</email><idno type="halauthor">59059</idno><affiliation ref="#struct-2580"></affiliation></author><editor role="depositor"><persName><forename>Publications</forename><surname>Loria</surname></persName><email>publications@loria.fr</email></editor></titleStmt><editionStmt><edition n="v1" type="current"><date type="whenSubmitted">2006-09-25 17:03:53</date><date type="whenModified">2016-05-19 01:05:35</date><date type="whenReleased">2006-09-28 15:22:44</date><date type="whenProduced">1998</date></edition><respStmt><resp>contributor</resp><name key="108626"><persName><forename>Publications</forename><surname>Loria</surname></persName><email>publications@loria.fr</email></name></respStmt></editionStmt><publicationStmt><distributor>CCSD</distributor><idno type="halId">inria-00098601</idno><idno type="halUri">https://hal.inria.fr/inria-00098601</idno><idno type="halBibtex">galmiche:inria-00098601</idno><idno type="halRefHtml">Theoretical Computer Science, Elsevier, 1998, 30 p</idno><idno type="halRef">Theoretical Computer Science, Elsevier, 1998, 30 p</idno></publicationStmt><seriesStmt><idno type="stamp" n="INRIA">INRIA - Institut National de Recherche en Informatique et en Automatique</idno><idno type="stamp" n="CNRS">CNRS - Centre national de la recherche scientifique</idno><idno type="stamp" n="LORIA2">Publications du LORIA</idno><idno type="stamp" n="LABO-LORIA-SET" p="LORIA">LABO-LORIA-SET</idno><idno type="stamp" n="LORIA">LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications</idno><idno type="stamp" n="LORIA-FM" p="LORIA">Méthodes formelles</idno><idno type="stamp" n="UNIV-LORRAINE">Université de Lorraine</idno><idno type="stamp" n="INPL">Institut National Polytechnique de Lorraine</idno></seriesStmt><notesStmt><note type="commentary">Article dans revue scientifique avec comité de lecture.</note><note type="audience" n="1">Not set</note><note type="popular" n="0">No</note><note type="peer" n="1">Yes</note></notesStmt><sourceDesc><biblStruct><analytic><title xml:lang="en">Connection proof search methods in Linear Logic and proof nets construction</title><author role="aut"><persName><forename type="first">Didier</forename><surname>Galmiche</surname></persName><email>galmiche@loria.fr</email><idno type="halAuthorId">59059</idno><affiliation ref="#struct-2580"></affiliation></author></analytic><monogr><idno type="localRef">98-R-126 || galmiche98c</idno><idno type="halJournalId" status="VALID">19594</idno><idno type="issn">0304-3975</idno><title level="j">Theoretical Computer Science</title><imprint><publisher>Elsevier</publisher><biblScope unit="pp">30 p</biblScope><date type="datePub">1998</date></imprint></monogr></biblStruct></sourceDesc><profileDesc><langUsage><language ident="en">English</language></langUsage><textClass><keywords scheme="author"><term xml:lang="fr">Méthode des connections</term><term xml:lang="fr">Automated deduction</term><term xml:lang="fr">Connection method</term><term xml:lang="fr">Linear Logic</term><term xml:lang="fr">Proof nets</term><term xml:lang="fr">Logique Linéaire</term><term xml:lang="fr">Réseaux de preuve</term><term xml:lang="fr">Déduction automatique</term></keywords><classCode scheme="halDomain" n="info.info-oh">Computer Science [cs]/Other [cs.OH]</classCode><classCode scheme="halTypology" n="ART">Journal articles</classCode></textClass><abstract xml:lang="en">In this paper we present proof search methods related with matrix (or connection) characterization of provability for fragments of Linear Logic (LL) and their relationships with automated proof and proof net construction. Non-classical logics as intuitionistic and linear logics are used in various branches of computer science and in many of these applications automated proof methods are needed. In LL the notion of proof net provides a nice, graphical representation of proofs (without some syntactical bureaucracy) and some works emphasized, for instance, the importance of proof nets to analyze evaluation strategies for proof normalization (and thus for computation) taking into account some concurrency and parallelism. We propose here a based on connection characterization of Multiplicative Linear Logic (MLL) and consequently a connection based proof search method that has the nice property to simultaneously construct a proof net (and also a sequent proof) which can be useful within proof environments. From these results, we expect to consider provability and proof nets construction in other LL fragments that are logical foundations of type-theoretic languages.</abstract></profileDesc></hal></record>Pour manipuler ce document sous Unix (Dilib)
EXPLOR_STEP=$WICRI_ROOT/Wicri/Lorraine/explor/InforLorV4/Data/Hal/Checkpoint
HfdSelect -h $EXPLOR_STEP/biblio.hfd -nk 006A10 | SxmlIndent | more
Ou
HfdSelect -h $EXPLOR_AREA/Data/Hal/Checkpoint/biblio.hfd -nk 006A10 | SxmlIndent | more
Pour mettre un lien sur cette page dans le réseau Wicri
{{Explor lien
|wiki= Wicri/Lorraine
|area= InforLorV4
|flux= Hal
|étape= Checkpoint
|type= RBID
|clé= Hal:inria-00098601
|texte= Connection proof search methods in Linear Logic and proof nets construction
}}
| This area was generated with Dilib version V0.6.33. |  |