InforLorV4, Main, Exploration, bibRecordById, Pascal:00-0103869

Connection methods in linear logic and proof nets construction

Identifieur interne : 009D56 ( Main/Exploration ); 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

Affiliations:

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>
<idno type="wicri:Area/Main/Exploration">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>
<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é Henri Poincaré</li>
</orgName>
</list>
<tree><country name="France"><region name="Grand Est"><name sortKey="Galmiche, D" sort="Galmiche, D" uniqKey="Galmiche D" first="D." last="Galmiche">D. Galmiche</name>
</region>
<name sortKey="Galmiche, D" sort="Galmiche, D" uniqKey="Galmiche D" first="D." last="Galmiche">D. Galmiche</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 009D56 | SxmlIndent | more

HfdSelect -h $EXPLOR_AREA/Data/Main/Exploration/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=   Exploration
   |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

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...)

Le document en format XML

Pour manipuler ce document sous Unix (Dilib)

Pour mettre un lien sur cette page dans le réseau Wicri

	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.