InforLorV4, PascalFrancis, Corpus, bibRecord, 000A66

Connection methods in linear logic and proof nets construction

Identifieur interne : 000A66 ( PascalFrancis/Corpus ); précédent : 000A65; suivant : 000A67

Connection methods in linear logic and proof nets construction

Auteurs : D. Galmiche

Source :

Theoretical computer science [ 0304-3975 ] ; 2000.

RBID : Pascal:00-0103869

Descripteurs français

Pascal (Inist)
- Programmation logique, Déduction, Théorie preuve, Complétude, Algorithme, Additif, Logique linéaire, Méthode connexion, Procédure décision, Réseau preuve.

English descriptors

KwdEn :
- Additive, Algorithm, Completeness, Connection method, Decision procedure, Deduction, Linear logic, Logical programming, Proof net, Proof theory.

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.

Notice en format standard (ISO 2709)

Pour connaître la documentation sur le format Inist Standard.

A01	`01`	`1`		`@0 0304-3975`
A02	`01`			`@0 TCSCDI`
A03		`1`		`@0 Theor. comput. sci.`
A05				`@2 232`
A06				`@2 1-2`
A08	`01`	`1`	`ENG`	`@1 Connection methods in linear logic and proof nets construction`
A09	`01`	`1`	`ENG`	`@1 Proof-search in Type-theoretic Languages`
A11	`01`	`1`		`@1 GALMICHE (D.)`
A12	`01`	`1`		`@1 GALMICHE (Didier) @9 ed.`
A12	`02`	`1`		`@1 PYM (David J.) @9 ed.`
A14	`01`			`@1 LORIA - Université Henri Poincaré, Campus Scientifique - B.P. 239 @2 54506 Vandœuvre-lès-Nancy @3 FRA @Z 1 aut.`
A15	`01`			`@1 LORIA - Université Henri Poincaré, Campus Scientifique, B.P. 239 @2 54506 Vandoeuvre-les-Nancy @3 FRA @Z 1 aut.`
A15	`02`			`@1 Queen Mary & Westfield College, Department of Computer Science, University of London, Mile End Road @2 London, E1 4NS @3 GBR @Z 2 aut.`
A20				`@1 231-272`
A21				`@1 2000`
A23	`01`			`@0 ENG`
A43	`01`			`@1 INIST @2 17243 @5 354000081470930080`
A44				`@0 0000 @1 © 2000 INIST-CNRS. All rights reserved.`
A45				`@0 48 ref.`
A47	`01`	`1`		`@0 00-0103869`
A60				`@1 P`
A61				`@0 A`
A64	`01`	`1`		`@0 Theoretical computer science`
A66	`01`			`@0 NLD`
C01	`01`		`ENG`	@0 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.
C02	`01`	`X`		`@0 001A02A01B`
C02	`02`	`X`		`@0 001A02A01D`
C02	`03`	`X`		`@0 001A02A01F`
C03	`01`	`X`	`FRE`	`@0 Programmation logique @5 01`
C03	`01`	`X`	`ENG`	`@0 Logical programming @5 01`
C03	`01`	`X`	`SPA`	`@0 Programación lógica @5 01`
C03	`02`	`X`	`FRE`	`@0 Déduction @5 02`
C03	`02`	`X`	`ENG`	`@0 Deduction @5 02`
C03	`02`	`X`	`SPA`	`@0 Deducción @5 02`
C03	`03`	`X`	`FRE`	`@0 Théorie preuve @5 03`
C03	`03`	`X`	`ENG`	`@0 Proof theory @5 03`
C03	`03`	`X`	`SPA`	`@0 Teoría demonstración @5 03`
C03	`04`	`X`	`FRE`	`@0 Complétude @5 04`
C03	`04`	`X`	`ENG`	`@0 Completeness @5 04`
C03	`04`	`X`	`SPA`	`@0 Completitud @5 04`
C03	`05`	`X`	`FRE`	`@0 Algorithme @5 05`
C03	`05`	`X`	`ENG`	`@0 Algorithm @5 05`
C03	`05`	`X`	`SPA`	`@0 Algoritmo @5 05`
C03	`06`	`X`	`FRE`	`@0 Additif @5 06`
C03	`06`	`X`	`ENG`	`@0 Additive @5 06`
C03	`06`	`X`	`SPA`	`@0 Aditivo @5 06`
C03	`07`	`X`	`FRE`	`@0 Logique linéaire @4 CD @5 96`
C03	`07`	`X`	`ENG`	`@0 Linear logic @4 CD @5 96`
C03	`08`	`X`	`FRE`	`@0 Méthode connexion @4 CD @5 97`
C03	`08`	`X`	`ENG`	`@0 Connection method @4 CD @5 97`
C03	`09`	`X`	`FRE`	`@0 Procédure décision @4 CD @5 98`
C03	`09`	`X`	`ENG`	`@0 Decision procedure @4 CD @5 98`
C03	`10`	`X`	`FRE`	`@0 Réseau preuve @4 CD @5 99`
C03	`10`	`X`	`ENG`	`@0 Proof net @4 CD @5 99`
N21				`@1 073`

Format Inist (serveur)

NO :	PASCAL 00-0103869 INIST
ET :	Connection methods in linear logic and proof nets construction
AU :	GALMICHE (D.); GALMICHE (Didier); PYM (David J.)
AF :	LORIA - Université Henri Poincaré, Campus Scientifique - B.P. 239/54506 Vandœuvre-lès-Nancy/France (1 aut.); LORIA - Université Henri Poincaré, Campus Scientifique, B.P. 239/54506 Vandoeuvre-les-Nancy/France (1 aut.); Queen Mary & Westfield College, Department of Computer Science, University of London, Mile End Road/London, E1 4NS/Royaume-Uni (2 aut.)
DT :	Publication en série; Niveau analytique
SO :	Theoretical computer science; ISSN 0304-3975; Coden TCSCDI; Pays-Bas; Da. 2000; Vol. 232; No. 1-2; Pp. 231-272; Bibl. 48 ref.
LA :	Anglais
EA :	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.
CC :	001A02A01B; 001A02A01D; 001A02A01F
FD :	Programmation logique; Déduction; Théorie preuve; Complétude; Algorithme; Additif; Logique linéaire; Méthode connexion; Procédure décision; Réseau preuve
ED :	Logical programming; Deduction; Proof theory; Completeness; Algorithm; Additive; Linear logic; Connection method; Decision procedure; Proof net
SD :	Programación lógica; Deducción; Teoría demonstración; Completitud; Algoritmo; Aditivo
LO :	INIST-17243.354000081470930080
ID :	00-0103869

Links to Exploration step

Pascal:00-0103869

Le document en format XML

<record><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><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>
</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>
</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><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>
</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><standard h6="B"><pA><fA01 i1="01" i2="1"><s0>0304-3975</s0>
</fA01>
<fA02 i1="01"><s0>TCSCDI</s0>
</fA02>
<fA03 i2="1"><s0>Theor. comput. sci.</s0>
</fA03>
<fA05><s2>232</s2>
</fA05>
<fA06><s2>1-2</s2>
</fA06>
<fA08 i1="01" i2="1" l="ENG"><s1>Connection methods in linear logic and proof nets construction</s1>
</fA08>
<fA09 i1="01" i2="1" l="ENG"><s1>Proof-search in Type-theoretic Languages</s1>
</fA09>
<fA11 i1="01" i2="1"><s1>GALMICHE (D.)</s1>
</fA11>
<fA12 i1="01" i2="1"><s1>GALMICHE (Didier)</s1>
<s9>ed.</s9>
</fA12>
<fA12 i1="02" i2="1"><s1>PYM (David J.)</s1>
<s9>ed.</s9>
</fA12>
<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>
</fA14>
<fA15 i1="01"><s1>LORIA - Université Henri Poincaré, Campus Scientifique, B.P. 239</s1>
<s2>54506 Vandoeuvre-les-Nancy</s2>
<s3>FRA</s3>
<sZ>1 aut.</sZ>
</fA15>
<fA15 i1="02"><s1>Queen Mary & Westfield College, Department of Computer Science, University of London, Mile End Road</s1>
<s2>London, E1 4NS</s2>
<s3>GBR</s3>
<sZ>2 aut.</sZ>
</fA15>
<fA20><s1>231-272</s1>
</fA20>
<fA21><s1>2000</s1>
</fA21>
<fA23 i1="01"><s0>ENG</s0>
</fA23>
<fA43 i1="01"><s1>INIST</s1>
<s2>17243</s2>
<s5>354000081470930080</s5>
</fA43>
<fA44><s0>0000</s0>
<s1>© 2000 INIST-CNRS. All rights reserved.</s1>
</fA44>
<fA45><s0>48 ref.</s0>
</fA45>
<fA47 i1="01" i2="1"><s0>00-0103869</s0>
</fA47>
<fA60><s1>P</s1>
</fA60>
<fA61><s0>A</s0>
</fA61>
<fA64 i1="01" i2="1"><s0>Theoretical computer science</s0>
</fA64>
<fA66 i1="01"><s0>NLD</s0>
</fA66>
<fC01 i1="01" l="ENG"><s0>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.</s0>
</fC01>
<fC02 i1="01" i2="X"><s0>001A02A01B</s0>
</fC02>
<fC02 i1="02" i2="X"><s0>001A02A01D</s0>
</fC02>
<fC02 i1="03" i2="X"><s0>001A02A01F</s0>
</fC02>
<fC03 i1="01" i2="X" l="FRE"><s0>Programmation logique</s0>
<s5>01</s5>
</fC03>
<fC03 i1="01" i2="X" l="ENG"><s0>Logical programming</s0>
<s5>01</s5>
</fC03>
<fC03 i1="01" i2="X" l="SPA"><s0>Programación lógica</s0>
<s5>01</s5>
</fC03>
<fC03 i1="02" i2="X" l="FRE"><s0>Déduction</s0>
<s5>02</s5>
</fC03>
<fC03 i1="02" i2="X" l="ENG"><s0>Deduction</s0>
<s5>02</s5>
</fC03>
<fC03 i1="02" i2="X" l="SPA"><s0>Deducción</s0>
<s5>02</s5>
</fC03>
<fC03 i1="03" i2="X" l="FRE"><s0>Théorie preuve</s0>
<s5>03</s5>
</fC03>
<fC03 i1="03" i2="X" l="ENG"><s0>Proof theory</s0>
<s5>03</s5>
</fC03>
<fC03 i1="03" i2="X" l="SPA"><s0>Teoría demonstración</s0>
<s5>03</s5>
</fC03>
<fC03 i1="04" i2="X" l="FRE"><s0>Complétude</s0>
<s5>04</s5>
</fC03>
<fC03 i1="04" i2="X" l="ENG"><s0>Completeness</s0>
<s5>04</s5>
</fC03>
<fC03 i1="04" i2="X" l="SPA"><s0>Completitud</s0>
<s5>04</s5>
</fC03>
<fC03 i1="05" i2="X" l="FRE"><s0>Algorithme</s0>
<s5>05</s5>
</fC03>
<fC03 i1="05" i2="X" l="ENG"><s0>Algorithm</s0>
<s5>05</s5>
</fC03>
<fC03 i1="05" i2="X" l="SPA"><s0>Algoritmo</s0>
<s5>05</s5>
</fC03>
<fC03 i1="06" i2="X" l="FRE"><s0>Additif</s0>
<s5>06</s5>
</fC03>
<fC03 i1="06" i2="X" l="ENG"><s0>Additive</s0>
<s5>06</s5>
</fC03>
<fC03 i1="06" i2="X" l="SPA"><s0>Aditivo</s0>
<s5>06</s5>
</fC03>
<fC03 i1="07" i2="X" l="FRE"><s0>Logique linéaire</s0>
<s4>CD</s4>
<s5>96</s5>
</fC03>
<fC03 i1="07" i2="X" l="ENG"><s0>Linear logic</s0>
<s4>CD</s4>
<s5>96</s5>
</fC03>
<fC03 i1="08" i2="X" l="FRE"><s0>Méthode connexion</s0>
<s4>CD</s4>
<s5>97</s5>
</fC03>
<fC03 i1="08" i2="X" l="ENG"><s0>Connection method</s0>
<s4>CD</s4>
<s5>97</s5>
</fC03>
<fC03 i1="09" i2="X" l="FRE"><s0>Procédure décision</s0>
<s4>CD</s4>
<s5>98</s5>
</fC03>
<fC03 i1="09" i2="X" l="ENG"><s0>Decision procedure</s0>
<s4>CD</s4>
<s5>98</s5>
</fC03>
<fC03 i1="10" i2="X" l="FRE"><s0>Réseau preuve</s0>
<s4>CD</s4>
<s5>99</s5>
</fC03>
<fC03 i1="10" i2="X" l="ENG"><s0>Proof net</s0>
<s4>CD</s4>
<s5>99</s5>
</fC03>
<fN21><s1>073</s1>
</fN21>
</pA>
</standard>
<server><NO>PASCAL 00-0103869 INIST</NO>
<ET>Connection methods in linear logic and proof nets construction</ET>
<AU>GALMICHE (D.); GALMICHE (Didier); PYM (David J.)</AU>
<AF>LORIA - Université Henri Poincaré, Campus Scientifique - B.P. 239/54506 Vandœuvre-lès-Nancy/France (1 aut.); LORIA - Université Henri Poincaré, Campus Scientifique, B.P. 239/54506 Vandoeuvre-les-Nancy/France (1 aut.); Queen Mary & Westfield College, Department of Computer Science, University of London, Mile End Road/London, E1 4NS/Royaume-Uni (2 aut.)</AF>
<DT>Publication en série; Niveau analytique</DT>
<SO>Theoretical computer science; ISSN 0304-3975; Coden TCSCDI; Pays-Bas; Da. 2000; Vol. 232; No. 1-2; Pp. 231-272; Bibl. 48 ref.</SO>
<LA>Anglais</LA>
<EA>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.</EA>
<CC>001A02A01B; 001A02A01D; 001A02A01F</CC>
<FD>Programmation logique; Déduction; Théorie preuve; Complétude; Algorithme; Additif; Logique linéaire; Méthode connexion; Procédure décision; Réseau preuve</FD>
<ED>Logical programming; Deduction; Proof theory; Completeness; Algorithm; Additive; Linear logic; Connection method; Decision procedure; Proof net</ED>
<SD>Programación lógica; Deducción; Teoría demonstración; Completitud; Algoritmo; Aditivo</SD>
<LO>INIST-17243.354000081470930080</LO>
<ID>00-0103869</ID>
</server>
</inist>
</record>

Pour manipuler ce document sous Unix (Dilib)

EXPLOR_STEP=$WICRI_ROOT/Wicri/Lorraine/explor/InforLorV4/Data/PascalFrancis/Corpus

HfdSelect -h $EXPLOR_STEP/biblio.hfd -nk 000A66 | SxmlIndent | more

HfdSelect -h $EXPLOR_AREA/Data/PascalFrancis/Corpus/biblio.hfd -nk 000A66 | SxmlIndent | more

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

{{Explor lien
   |wiki=    Wicri/Lorraine
   |area=    InforLorV4
   |flux=    PascalFrancis
   |étape=   Corpus
   |type=    RBID
   |clé=     Pascal:00-0103869
   |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

Notice en format standard (ISO 2709)

Format Inist (serveur)

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