A procedure for automatic proof nets construction
Identifieur interne : 00DF97 ( Main/Merge ); précédent : 00DF96; suivant : 00DF98A procedure for automatic proof nets construction
Auteurs : Didier Galmiche [France] ; Guy Perrier [France]Source :
English descriptors
- mix :
Abstract
In this paper, we consider multiplicative linear logic (MLL) from an automated deduction point of view. Linear logic is more expressive than classical and intuitionistic logic and has an undirectional character due to the particular treatment of negation and the absence of structural rules. Considering this new logical framework to make logic programming or programming with proofs (extracting programs from proofs), a better comprehension of proofs in MLL (proof nets) is necessary and automated deduction has to be studied. Knowing that the multiplicative part of linear logic is decidable, we propose a new algorithm to construct automatically a proof net for a given sequent in MLL with proofs of termination, correctness and completeness. It can be considered as a more direct and implementation oriented way to consider automated deduction in linear logic.
Url:
Links toward previous steps (curation, corpus...)
- to stream Hal, to step Corpus: 000830
- to stream Hal, to step Curation: 000830
- to stream Hal, to step Checkpoint: 006C54
Links to Exploration step
Hal:hal-01297750Le document en format XML
<record><TEI><teiHeader><fileDesc><titleStmt><title xml:lang="en">A procedure for automatic 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="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></hal:affiliation><country>France</country></affiliation></author><author><name sortKey="Perrier, Guy" sort="Perrier, Guy" uniqKey="Perrier G" first="Guy" last="Perrier">Guy Perrier</name><affiliation wicri:level="1"><hal:affiliation type="researchteam" xml:id="struct-454503" status="OLD"><orgName>Prograis</orgName><desc><address><country key="FR"></country></address></desc><listRelation><relation active="#struct-2496" type="direct"></relation><relation active="#struct-300009" type="indirect"></relation><relation active="#struct-133218" type="direct"></relation><relation active="#struct-441569" type="indirect"></relation></listRelation><tutelles><tutelle active="#struct-2496" type="direct"><org type="laboratory" xml:id="struct-2496" status="OLD"><orgName>INRIA Lorraine</orgName><desc><address><addrLine>615 rue du Jardin Botanique 54600 Villers-lès-Nancy</addrLine><country key="FR"></country></address><ref type="url">http://www.inria.fr/centre-de-recherche-inria/nancy-grand-est</ref></desc><listRelation><relation active="#struct-300009" type="direct"></relation></listRelation></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-133218" type="direct"><org type="laboratory" xml:id="struct-133218" status="OLD"><orgName>Centre de Recherche en Informatique de Nancy</orgName><orgName type="acronym">CRIN</orgName><desc><address><addrLine>CRIN RFIA Campus Scientifique B.P. 239 54506 Vandoeuvre-Les-Nancy</addrLine><country key="FR"></country></address></desc><listRelation><relation active="#struct-441569" type="direct"></relation></listRelation></org></tutelle><tutelle 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></tutelles></hal:affiliation><country>France</country></affiliation></author></titleStmt><publicationStmt><idno type="wicri:source">HAL</idno><idno type="RBID">Hal:hal-01297750</idno><idno type="halId">hal-01297750</idno><idno type="halUri">https://hal.inria.fr/hal-01297750</idno><idno type="url">https://hal.inria.fr/hal-01297750</idno><date when="1992">1992</date><idno type="wicri:Area/Hal/Corpus">000830</idno><idno type="wicri:Area/Hal/Curation">000830</idno><idno type="wicri:Area/Hal/Checkpoint">006C54</idno><idno type="wicri:explorRef" wicri:stream="Hal" wicri:step="Checkpoint">006C54</idno><idno type="wicri:Area/Main/Merge">00DF97</idno></publicationStmt><sourceDesc><biblStruct><analytic><title xml:lang="en">A procedure for automatic 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="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></hal:affiliation><country>France</country></affiliation></author><author><name sortKey="Perrier, Guy" sort="Perrier, Guy" uniqKey="Perrier G" first="Guy" last="Perrier">Guy Perrier</name><affiliation wicri:level="1"><hal:affiliation type="researchteam" xml:id="struct-454503" status="OLD"><orgName>Prograis</orgName><desc><address><country key="FR"></country></address></desc><listRelation><relation active="#struct-2496" type="direct"></relation><relation active="#struct-300009" type="indirect"></relation><relation active="#struct-133218" type="direct"></relation><relation active="#struct-441569" type="indirect"></relation></listRelation><tutelles><tutelle active="#struct-2496" type="direct"><org type="laboratory" xml:id="struct-2496" status="OLD"><orgName>INRIA Lorraine</orgName><desc><address><addrLine>615 rue du Jardin Botanique 54600 Villers-lès-Nancy</addrLine><country key="FR"></country></address><ref type="url">http://www.inria.fr/centre-de-recherche-inria/nancy-grand-est</ref></desc><listRelation><relation active="#struct-300009" type="direct"></relation></listRelation></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-133218" type="direct"><org type="laboratory" xml:id="struct-133218" status="OLD"><orgName>Centre de Recherche en Informatique de Nancy</orgName><orgName type="acronym">CRIN</orgName><desc><address><addrLine>CRIN RFIA Campus Scientifique B.P. 239 54506 Vandoeuvre-Les-Nancy</addrLine><country key="FR"></country></address></desc><listRelation><relation active="#struct-441569" type="direct"></relation></listRelation></org></tutelle><tutelle 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></tutelles></hal:affiliation><country>France</country></affiliation></author></analytic></biblStruct></sourceDesc></fileDesc><profileDesc><textClass><keywords scheme="mix" xml:lang="en"><term>Linear Logic</term><term>Proof nets</term></keywords></textClass></profileDesc></teiHeader><front><div type="abstract" xml:lang="en">In this paper, we consider multiplicative linear logic (MLL) from an automated deduction point of view. Linear logic is more expressive than classical and intuitionistic logic and has an undirectional character due to the particular treatment of negation and the absence of structural rules. Considering this new logical framework to make logic programming or programming with proofs (extracting programs from proofs), a better comprehension of proofs in MLL (proof nets) is necessary and automated deduction has to be studied. Knowing that the multiplicative part of linear logic is decidable, we propose a new algorithm to construct automatically a proof net for a given sequent in MLL with proofs of termination, correctness and completeness. It can be considered as a more direct and implementation oriented way to consider automated deduction in linear logic.</div></front></TEI></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 00DF97 | SxmlIndent | more
Ou
HfdSelect -h $EXPLOR_AREA/Data/Main/Merge/biblio.hfd -nk 00DF97 | 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é= Hal:hal-01297750
|texte= A procedure for automatic proof nets construction
}}
| This area was generated with Dilib version V0.6.33. |  |