Connection methods in linear logic and proof nets construction
Identifieur interne : 00A622 ( Main/Merge ); précédent : 00A621; suivant : 00A623Connection methods in linear logic and proof nets construction
Auteurs : D. Galmiche [France]Source :
- Theoretical computer science [ 0304-3975 ] ; 2000.
Descripteurs français
- Pascal (Inist)
English descriptors
- KwdEn :
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.
Links toward previous steps (curation, corpus...)
- to stream PascalFrancis, to step Corpus: 000A66
- to stream PascalFrancis, to step Curation: 000016
- to stream PascalFrancis, to step Checkpoint: 000A16
Links to Exploration step
Pascal:00-0103869Le 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 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><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></country></tree></affiliations></record>Pour manipuler ce document sous Unix (Dilib)
EXPLOR_STEP=$WICRI_ROOT/Wicri/Lorraine/explor/InforLorV4/Data/Main/Merge
HfdSelect -h $EXPLOR_STEP/biblio.hfd -nk 00A622 | SxmlIndent | more
Ou
HfdSelect -h $EXPLOR_AREA/Data/Main/Merge/biblio.hfd -nk 00A622 | SxmlIndent | more
Pour mettre un lien sur cette page dans le réseau Wicri
{{Explor lien
|wiki= Wicri/Lorraine
|area= InforLorV4
|flux= Main
|étape= Merge
|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. |  |