InforLorV4, Main, Curation, bibRecord, 009D56

Connection methods in linear logic and proof nets construction

Identifieur interne : 009D56 ( Main/Curation ); précédent : 009D55; suivant : 009D57

Connection methods in linear logic and proof nets construction

Auteurs : D. Galmiche [France]

Source :

Theoretical Computer Science [ 0304-3975 ] ; 2000.

RBID : ISTEX:EA0153F44D7107BDFAA20F725DB634FB7B1CB692

Descripteurs français

Pascal (Inist)
- Additif, Algorithme, Complétude, Déduction, Logique linéaire, Méthode connexion, Procédure décision, Programmation logique, Réseau preuve, Théorie preuve.
mix :
- automated deduction, connection methods, déduction automatique, linear logic, logique linéaire, méthodes des connexions, proof nets, réseaux de preuve.

English descriptors

KwdEn :
- Additive, Algorithm, Completeness, Connection method, Decision procedure, Deduction, Linear logic, Logical programming, Proof net, Proof theory.
Teeft :
- Additive, Additive connectives, Additive sequent, Algorithm, Analyse, Analytic tableaux, Atomic formula, Atomic formulae, Atomic path, Atomic paths, Axiom, Calculus, Canonical, Canonical proof, Cient, Classical logic, Complementary connection, Comput, Computer science, Conjunctive, Conjunctive subformula, Connection characterization, Connection method, Connection methods, Connection structure, Decision procedure, Decomposition tree, Direct logic, Erent, Formula tree, Fragment, Free leaf, Galmiche, Girard, Inductive, Inductive construction, Inference rules, Initial sequent, Intuitionistic, Intuitionistic logic, Intuitionistic logics, Inverse method, July, Lecture notes, Linear logic, Linear sequent calculus, Logic, Logical foundations, Main result, Mall fragment, Matrix, Minimal path, Multiplicative, Permutability results, Proof, Proof construction, Proof nets, Proof nets construction, Proof search, Proof structure, Proof structures, Provability, Provable, Resp, Same element, Search space, Second premise, Sequent, Sequent calculus, Sequent proof, Sequent reconstruction, Sequents, Special rules, Special type, Springer, Subformula, Subformulae, Subnets, Subset, Tableau.

Abstract

Abstract: Linear logic (LL) is the logical foundation of some type-theoretic languages and also of environments for specification and theorem proving. In this paper, we analyse the relationships between the proof net notion of LL and the connection notion used for efficient proof search in different logics. Aiming at using proof nets as a tool for automated deduction in linear logic, we define a connection-based characterization of provability in Multiplicative Linear Logic (MLL). We show that an algorithm for proof net construction can be seen as a proof-search connection method. This central result is illustrated with a specific algorithm that is able to construct, for a provable MLL sequent, a set of connections, a proof net and a sequent proof. From these results we expect to extend to other LL fragments, we analyse what happens with the additive connectives of LL by tackling the additive fragment in a similar way.

Url:

DOI: 10.1016/S0304-3975(99)00176-0

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

to stream Istex, to step Corpus: Pour aller vers cette notice dans l'étape Curation :003801
to stream Istex, to step Curation: Pour aller vers cette notice dans l'étape Curation :003758
to stream Istex, to step Checkpoint: Pour aller vers cette notice dans l'étape Curation :002009
to stream Main, to step Merge: Pour aller vers cette notice dans l'étape Curation :00A337
to stream Hal, to step Corpus: Pour aller vers cette notice dans l'étape Curation :001841
to stream Hal, to step Curation: Pour aller vers cette notice dans l'étape Curation :001841
to stream Hal, to step Checkpoint: Pour aller vers cette notice dans l'étape Curation :006282
to stream Main, to step Merge: Pour aller vers cette notice dans l'étape Curation :00A912
to stream PascalFrancis, to step Corpus: Pour aller vers cette notice dans l'étape Curation :000A66
to stream PascalFrancis, to step Curation: Pour aller vers cette notice dans l'étape Curation :000016
to stream PascalFrancis, to step Checkpoint: Pour aller vers cette notice dans l'étape Curation :000A16
to stream Main, to step Merge: Pour aller vers cette notice dans l'étape Curation :00A622

Links to Exploration step

ISTEX:EA0153F44D7107BDFAA20F725DB634FB7B1CB692

Le document en format XML

<record><TEI wicri:istexFullTextTei="biblStruct"><teiHeader><fileDesc><titleStmt><title>Connection methods in linear logic and proof nets construction</title>
<author><name sortKey="Galmiche, D" sort="Galmiche, D" uniqKey="Galmiche D" first="D." last="Galmiche">D. Galmiche</name>
</author>
</titleStmt>
<publicationStmt><idno type="wicri:source">ISTEX</idno>
<idno type="RBID">ISTEX:EA0153F44D7107BDFAA20F725DB634FB7B1CB692</idno>
<date when="2000" year="2000">2000</date>
<idno type="doi">10.1016/S0304-3975(99)00176-0</idno>
<idno type="url">https://api.istex.fr/ark:/67375/6H6-6PPV5FNH-5/fulltext.pdf</idno>
<idno type="wicri:Area/Istex/Corpus">003801</idno>
<idno type="wicri:explorRef" wicri:stream="Istex" wicri:step="Corpus" wicri:corpus="ISTEX">003801</idno>
<idno type="wicri:Area/Istex/Curation">003758</idno>
<idno type="wicri:Area/Istex/Checkpoint">002009</idno>
<idno type="wicri:explorRef" wicri:stream="Istex" wicri:step="Checkpoint">002009</idno>
<idno type="wicri:doubleKey">0304-3975:2000:Galmiche D:connection:methods:in</idno>
<idno type="wicri:Area/Main/Merge">00A337</idno>
<idno type="wicri:source">HAL</idno>
<idno type="RBID">Hal:inria-00099205</idno>
<idno type="url">https://hal.inria.fr/inria-00099205</idno>
<idno type="wicri:Area/Hal/Corpus">001841</idno>
<idno type="wicri:Area/Hal/Curation">001841</idno>
<idno type="wicri:Area/Hal/Checkpoint">006282</idno>
<idno type="wicri:explorRef" wicri:stream="Hal" wicri:step="Checkpoint">006282</idno>
<idno type="wicri:doubleKey">0304-3975:2000:Galmiche D:connection:methods:in</idno>
<idno type="wicri:Area/Main/Merge">00A912</idno>
<idno type="wicri:source">INIST</idno>
<idno type="RBID">Pascal:00-0103869</idno>
<idno type="wicri:Area/PascalFrancis/Corpus">000A66</idno>
<idno type="wicri:Area/PascalFrancis/Curation">000016</idno>
<idno type="wicri:Area/PascalFrancis/Checkpoint">000A16</idno>
<idno type="wicri:explorRef" wicri:stream="PascalFrancis" wicri:step="Checkpoint">000A16</idno>
<idno type="wicri:doubleKey">0304-3975:2000:Galmiche D:connection:methods:in</idno>
<idno type="wicri:Area/Main/Merge">00A622</idno>
<idno type="wicri:Area/Main/Curation">009D56</idno>
</publicationStmt>
<sourceDesc><biblStruct><analytic><title level="a">Connection methods in linear logic and proof nets construction</title>
<author><name sortKey="Galmiche, D" sort="Galmiche, D" uniqKey="Galmiche D" first="D." last="Galmiche">D. Galmiche</name>
<affiliation wicri:level="4"><country xml:lang="fr">France</country>
<wicri:regionArea>LORIA – Université Henri Poincaré, Campus Scientifique – B.P. 239, 54506 Vandœuvre-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é Henri Poincaré</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="2000">2000</date>
<biblScope unit="volume">232</biblScope>
<biblScope unit="issue">1–2</biblScope>
<biblScope unit="page" from="231">231</biblScope>
<biblScope unit="page" to="272">272</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>Additive</term>
<term>Algorithm</term>
<term>Completeness</term>
<term>Connection method</term>
<term>Decision procedure</term>
<term>Deduction</term>
<term>Linear logic</term>
<term>Logical programming</term>
<term>Proof net</term>
<term>Proof theory</term>
</keywords>
<keywords scheme="Pascal" xml:lang="fr"><term>Additif</term>
<term>Algorithme</term>
<term>Complétude</term>
<term>Déduction</term>
<term>Logique linéaire</term>
<term>Méthode connexion</term>
<term>Procédure décision</term>
<term>Programmation logique</term>
<term>Réseau preuve</term>
<term>Théorie preuve</term>
</keywords>
<keywords scheme="Teeft" xml:lang="en"><term>Additive</term>
<term>Additive connectives</term>
<term>Additive sequent</term>
<term>Algorithm</term>
<term>Analyse</term>
<term>Analytic tableaux</term>
<term>Atomic formula</term>
<term>Atomic formulae</term>
<term>Atomic path</term>
<term>Atomic paths</term>
<term>Axiom</term>
<term>Calculus</term>
<term>Canonical</term>
<term>Canonical proof</term>
<term>Cient</term>
<term>Classical logic</term>
<term>Complementary connection</term>
<term>Comput</term>
<term>Computer science</term>
<term>Conjunctive</term>
<term>Conjunctive subformula</term>
<term>Connection characterization</term>
<term>Connection method</term>
<term>Connection methods</term>
<term>Connection structure</term>
<term>Decision procedure</term>
<term>Decomposition tree</term>
<term>Direct logic</term>
<term>Erent</term>
<term>Formula tree</term>
<term>Fragment</term>
<term>Free leaf</term>
<term>Galmiche</term>
<term>Girard</term>
<term>Inductive</term>
<term>Inductive construction</term>
<term>Inference rules</term>
<term>Initial sequent</term>
<term>Intuitionistic</term>
<term>Intuitionistic logic</term>
<term>Intuitionistic logics</term>
<term>Inverse method</term>
<term>July</term>
<term>Lecture notes</term>
<term>Linear logic</term>
<term>Linear sequent calculus</term>
<term>Logic</term>
<term>Logical foundations</term>
<term>Main result</term>
<term>Mall fragment</term>
<term>Matrix</term>
<term>Minimal path</term>
<term>Multiplicative</term>
<term>Permutability results</term>
<term>Proof</term>
<term>Proof construction</term>
<term>Proof nets</term>
<term>Proof nets construction</term>
<term>Proof search</term>
<term>Proof structure</term>
<term>Proof structures</term>
<term>Provability</term>
<term>Provable</term>
<term>Resp</term>
<term>Same element</term>
<term>Search space</term>
<term>Second premise</term>
<term>Sequent</term>
<term>Sequent calculus</term>
<term>Sequent proof</term>
<term>Sequent reconstruction</term>
<term>Sequents</term>
<term>Special rules</term>
<term>Special type</term>
<term>Springer</term>
<term>Subformula</term>
<term>Subformulae</term>
<term>Subnets</term>
<term>Subset</term>
<term>Tableau</term>
</keywords>
<keywords scheme="mix" xml:lang="fr"><term>automated deduction</term>
<term>connection methods</term>
<term>déduction automatique</term>
<term>linear logic</term>
<term>logique linéaire</term>
<term>méthodes des connexions</term>
<term>proof nets</term>
<term>réseaux de preuve</term>
</keywords>
</textClass>
<langUsage><language ident="en">en</language>
</langUsage>
</profileDesc>
</teiHeader>
<front><div type="abstract" xml:lang="en">Abstract: Linear logic (LL) is the logical foundation of some type-theoretic languages and also of environments for specification and theorem proving. In this paper, we analyse the relationships between the proof net notion of LL and the connection notion used for efficient proof search in different logics. Aiming at using proof nets as a tool for automated deduction in linear logic, we define a connection-based characterization of provability in Multiplicative Linear Logic (MLL). We show that an algorithm for proof net construction can be seen as a proof-search connection method. This central result is illustrated with a specific algorithm that is able to construct, for a provable MLL sequent, a set of connections, a proof net and a sequent proof. From these results we expect to extend to other LL fragments, we analyse what happens with the additive connectives of LL by tackling the additive fragment in a similar way.</div>
</front>
</TEI>
<double idat="0304-3975:2000:Galmiche D:connection:methods:in"><HAL><TEI><teiHeader><fileDesc><titleStmt><title xml:lang="en">Connection 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-00099205</idno>
<idno type="halId">inria-00099205</idno>
<idno type="halUri">https://hal.inria.fr/inria-00099205</idno>
<idno type="url">https://hal.inria.fr/inria-00099205</idno>
<date when="2000">2000</date>
<idno type="wicri:Area/Hal/Corpus">001841</idno>
<idno type="wicri:Area/Hal/Curation">001841</idno>
<idno type="wicri:Area/Hal/Checkpoint">006282</idno>
<idno type="wicri:explorRef" wicri:stream="Hal" wicri:step="Checkpoint">006282</idno>
<idno type="wicri:doubleKey">0304-3975:2000:Galmiche D:connection:methods:in</idno>
<idno type="wicri:Area/Main/Merge">00A912</idno>
</publicationStmt>
<sourceDesc><biblStruct><analytic><title xml:lang="en">Connection 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">2000</date>
</imprint>
</series>
</biblStruct>
</sourceDesc>
</fileDesc>
<profileDesc><textClass><keywords scheme="mix" xml:lang="fr"><term>automated deduction</term>
<term>connection methods</term>
<term>déduction automatique</term>
<term>linear logic</term>
<term>logique linéaire</term>
<term>méthodes des connexions</term>
<term>proof nets</term>
<term>réseaux de preuve</term>
</keywords>
</textClass>
</profileDesc>
</teiHeader>
<front><div type="abstract" xml:lang="en">Linear logic (LL) is the logical foundation of some type-theoretic languages and also of environments for specification and theorem proving. In this paper, we analyse the relationships between the proof net notion of LL and the connection notion used for efficient proof-search in different logics. Aiming at using proof nets as a tool for automated deduction in linear logic, we define a connection-based characterization of provability in Multiplicative Linear Logic (MLL). We show that an algorithm for proof net construction can be seen as a proof-search connection method. This central result is illustrated with a specific algorithm that is able to construct, for a provable MLL sequent,a set of connections, a proof net and a sequent proof. From these results we expect to extend to other LL fragments, we analyse what happens with the additive connectives of LL by tackling the additive fragment in a similar way.</div>
</front>
</TEI>
</HAL>
<INIST><TEI><teiHeader><fileDesc><titleStmt><title xml:lang="en" level="a">Connection methods in linear logic and proof nets construction</title>
<author><name sortKey="Galmiche, D" sort="Galmiche, D" uniqKey="Galmiche D" first="D." last="Galmiche">D. Galmiche</name>
<affiliation wicri:level="4"><inist:fA14 i1="01"><s1>LORIA - Université Henri Poincaré, Campus Scientifique - B.P. 239</s1>
<s2>54506 Vandœuvre-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é Henri Poincaré</orgName>
</affiliation>
</author>
</titleStmt>
<publicationStmt><idno type="wicri:source">INIST</idno>
<idno type="inist">00-0103869</idno>
<date when="2000">2000</date>
<idno type="stanalyst">PASCAL 00-0103869 INIST</idno>
<idno type="RBID">Pascal:00-0103869</idno>
<idno type="wicri:Area/PascalFrancis/Corpus">000A66</idno>
<idno type="wicri:Area/PascalFrancis/Curation">000016</idno>
<idno type="wicri:Area/PascalFrancis/Checkpoint">000A16</idno>
<idno type="wicri:explorRef" wicri:stream="PascalFrancis" wicri:step="Checkpoint">000A16</idno>
<idno type="wicri:doubleKey">0304-3975:2000:Galmiche D:connection:methods:in</idno>
<idno type="wicri:Area/Main/Merge">00A622</idno>
</publicationStmt>
<sourceDesc><biblStruct><analytic><title xml:lang="en" level="a">Connection methods in linear logic and proof nets construction</title>
<author><name sortKey="Galmiche, D" sort="Galmiche, D" uniqKey="Galmiche D" first="D." last="Galmiche">D. Galmiche</name>
<affiliation wicri:level="4"><inist:fA14 i1="01"><s1>LORIA - Université Henri Poincaré, Campus Scientifique - B.P. 239</s1>
<s2>54506 Vandœuvre-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é Henri Poincaré</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="2000">2000</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>Additive</term>
<term>Algorithm</term>
<term>Completeness</term>
<term>Connection method</term>
<term>Decision procedure</term>
<term>Deduction</term>
<term>Linear logic</term>
<term>Logical programming</term>
<term>Proof net</term>
<term>Proof theory</term>
</keywords>
<keywords scheme="Pascal" xml:lang="fr"><term>Programmation logique</term>
<term>Déduction</term>
<term>Théorie preuve</term>
<term>Complétude</term>
<term>Algorithme</term>
<term>Additif</term>
<term>Logique linéaire</term>
<term>Méthode connexion</term>
<term>Procédure décision</term>
<term>Réseau preuve</term>
</keywords>
</textClass>
</profileDesc>
</teiHeader>
<front><div type="abstract" xml:lang="en">Linear logic (LL) is the logical foundation of some type-theoretic languages and also of environments for specification and theorem proving. In this paper, we analyse the relationships between the proof net notion of LL and the connection notion used for efficient proof search in different logics. Aiming at using proof nets as a tool for automated deduction in linear logic, we define a connection-based characterization of provability in Multiplicative Linear Logic (MLL). We show that an algorithm for proof net construction can be seen as a proof-search connection method. This central result is illustrated with a specific algorithm that is able to construct, for a provable MLL sequent, a set of connections, a proof net and a sequent proof. From these results we expect to extend to other LL fragments, we analyse what happens with the additive connectives of LL by tackling the additive fragment in a similar way.</div>
</front>
</TEI>
</INIST>
<ISTEX><TEI wicri:istexFullTextTei="biblStruct"><teiHeader><fileDesc><titleStmt><title>Connection methods in linear logic and proof nets construction</title>
<author><name sortKey="Galmiche, D" sort="Galmiche, D" uniqKey="Galmiche D" first="D." last="Galmiche">D. Galmiche</name>
</author>
</titleStmt>
<publicationStmt><idno type="wicri:source">ISTEX</idno>
<idno type="RBID">ISTEX:EA0153F44D7107BDFAA20F725DB634FB7B1CB692</idno>
<date when="2000" year="2000">2000</date>
<idno type="doi">10.1016/S0304-3975(99)00176-0</idno>
<idno type="url">https://api.istex.fr/ark:/67375/6H6-6PPV5FNH-5/fulltext.pdf</idno>
<idno type="wicri:Area/Istex/Corpus">003801</idno>
<idno type="wicri:explorRef" wicri:stream="Istex" wicri:step="Corpus" wicri:corpus="ISTEX">003801</idno>
<idno type="wicri:Area/Istex/Curation">003758</idno>
<idno type="wicri:Area/Istex/Checkpoint">002009</idno>
<idno type="wicri:explorRef" wicri:stream="Istex" wicri:step="Checkpoint">002009</idno>
<idno type="wicri:doubleKey">0304-3975:2000:Galmiche D:connection:methods:in</idno>
<idno type="wicri:Area/Main/Merge">00A337</idno>
</publicationStmt>
<sourceDesc><biblStruct><analytic><title level="a">Connection methods in linear logic and proof nets construction</title>
<author><name sortKey="Galmiche, D" sort="Galmiche, D" uniqKey="Galmiche D" first="D." last="Galmiche">D. Galmiche</name>
<affiliation wicri:level="4"><country xml:lang="fr">France</country>
<wicri:regionArea>LORIA – Université Henri Poincaré, Campus Scientifique – B.P. 239, 54506 Vandœuvre-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é Henri Poincaré</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="2000">2000</date>
<biblScope unit="volume">232</biblScope>
<biblScope unit="issue">1–2</biblScope>
<biblScope unit="page" from="231">231</biblScope>
<biblScope unit="page" to="272">272</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 connectives</term>
<term>Additive sequent</term>
<term>Algorithm</term>
<term>Analyse</term>
<term>Analytic tableaux</term>
<term>Atomic formula</term>
<term>Atomic formulae</term>
<term>Atomic path</term>
<term>Atomic paths</term>
<term>Axiom</term>
<term>Calculus</term>
<term>Canonical</term>
<term>Canonical proof</term>
<term>Cient</term>
<term>Classical logic</term>
<term>Complementary connection</term>
<term>Comput</term>
<term>Computer science</term>
<term>Conjunctive</term>
<term>Conjunctive subformula</term>
<term>Connection characterization</term>
<term>Connection method</term>
<term>Connection methods</term>
<term>Connection structure</term>
<term>Decision procedure</term>
<term>Decomposition tree</term>
<term>Direct logic</term>
<term>Erent</term>
<term>Formula tree</term>
<term>Fragment</term>
<term>Free leaf</term>
<term>Galmiche</term>
<term>Girard</term>
<term>Inductive</term>
<term>Inductive construction</term>
<term>Inference rules</term>
<term>Initial sequent</term>
<term>Intuitionistic</term>
<term>Intuitionistic logic</term>
<term>Intuitionistic logics</term>
<term>Inverse method</term>
<term>July</term>
<term>Lecture notes</term>
<term>Linear logic</term>
<term>Linear sequent calculus</term>
<term>Logic</term>
<term>Logical foundations</term>
<term>Main result</term>
<term>Mall fragment</term>
<term>Matrix</term>
<term>Minimal path</term>
<term>Multiplicative</term>
<term>Permutability results</term>
<term>Proof</term>
<term>Proof construction</term>
<term>Proof nets</term>
<term>Proof nets construction</term>
<term>Proof search</term>
<term>Proof structure</term>
<term>Proof structures</term>
<term>Provability</term>
<term>Provable</term>
<term>Resp</term>
<term>Same element</term>
<term>Search space</term>
<term>Second premise</term>
<term>Sequent</term>
<term>Sequent calculus</term>
<term>Sequent proof</term>
<term>Sequent reconstruction</term>
<term>Sequents</term>
<term>Special rules</term>
<term>Special type</term>
<term>Springer</term>
<term>Subformula</term>
<term>Subformulae</term>
<term>Subnets</term>
<term>Subset</term>
<term>Tableau</term>
</keywords>
</textClass>
<langUsage><language ident="en">en</language>
</langUsage>
</profileDesc>
</teiHeader>
<front><div type="abstract" xml:lang="en">Abstract: Linear logic (LL) is the logical foundation of some type-theoretic languages and also of environments for specification and theorem proving. In this paper, we analyse the relationships between the proof net notion of LL and the connection notion used for efficient proof search in different logics. Aiming at using proof nets as a tool for automated deduction in linear logic, we define a connection-based characterization of provability in Multiplicative Linear Logic (MLL). We show that an algorithm for proof net construction can be seen as a proof-search connection method. This central result is illustrated with a specific algorithm that is able to construct, for a provable MLL sequent, a set of connections, a proof net and a sequent proof. From these results we expect to extend to other LL fragments, we analyse what happens with the additive connectives of LL by tackling the additive fragment in a similar way.</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 009D56 | SxmlIndent | more

HfdSelect -h $EXPLOR_AREA/Data/Main/Curation/biblio.hfd -nk 009D56 | 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:EA0153F44D7107BDFAA20F725DB634FB7B1CB692
   |texte=   Connection methods in linear logic and proof nets construction
}}

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

Connection methods in linear logic and proof nets construction

Connection methods in linear logic and proof nets construction

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