A procedure for automatic proof nets construction
Identifieur interne : 000830 ( Hal/Corpus ); précédent : 000829; suivant : 000831A procedure for automatic proof nets construction
Auteurs : Didier Galmiche ; Guy PerrierSource :
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 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><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></affiliation></author><author><name sortKey="Perrier, Guy" sort="Perrier, Guy" uniqKey="Perrier G" first="Guy" last="Perrier">Guy Perrier</name><affiliation><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></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></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><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></affiliation></author><author><name sortKey="Perrier, Guy" sort="Perrier, Guy" uniqKey="Perrier G" first="Guy" last="Perrier">Guy Perrier</name><affiliation><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></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><hal api="V3"><titleStmt><title xml:lang="en">A procedure for automatic proof nets construction</title><author role="aut"><persName><forename type="first">Didier</forename><surname>Galmiche</surname></persName><email>galmiche@loria.fr</email><idno type="halauthor">59059</idno><affiliation ref="#struct-300291"></affiliation><affiliation ref="#struct-454503"></affiliation></author><author role="aut"><persName><forename type="first">Guy</forename><surname>Perrier</surname></persName><email>perrier@loria.fr</email><idno type="idhal">guy-perrier</idno><idno type="halauthor">59311</idno><affiliation ref="#struct-454503"></affiliation><affiliation ref="#struct-300291"></affiliation></author><editor role="depositor"><persName><forename>Guy</forename><surname>Perrier</surname></persName><email>guy.perrier@loria.fr</email></editor></titleStmt><editionStmt><edition n="v1" type="current"><date type="whenSubmitted">2016-04-04 17:37:08</date><date type="whenModified">2016-05-14 01:05:34</date><date type="whenReleased">2016-05-13 17:20:37</date><date type="whenProduced">1992</date><date type="whenEndEmbargoed">2016-04-04</date><ref type="file" target="https://hal.inria.fr/hal-01297750/document"><date notBefore="2016-04-04"></date></ref><ref type="file" subtype="author" n="1" target="https://hal.inria.fr/hal-01297750/file/lpar1992.pdf"><date notBefore="2016-04-04"></date></ref></edition><respStmt><resp>contributor</resp><name key="103193"><persName><forename>Guy</forename><surname>Perrier</surname></persName><email>guy.perrier@loria.fr</email></name></respStmt></editionStmt><publicationStmt><distributor>CCSD</distributor><idno type="halId">hal-01297750</idno><idno type="halUri">https://hal.inria.fr/hal-01297750</idno><idno type="halBibtex">galmiche:hal-01297750</idno><idno type="halRefHtml">Conference on Logic Programming and Automated Reasoning, LPAR'92, 1992, St-Petersburg, Russia. 624, pp.42-53, 1992, LNCS</idno><idno type="halRef">Conference on Logic Programming and Automated Reasoning, LPAR'92, 1992, St-Petersburg, Russia. 624, pp.42-53, 1992, LNCS</idno></publicationStmt><seriesStmt><idno type="stamp" n="CNRS">CNRS - Centre national de la recherche scientifique</idno><idno type="stamp" n="INRIA-LORRAINE">INRIA Nancy - Grand Est</idno><idno type="stamp" n="INRIA-NANCY-GRAND-EST">INRIA Nancy - Grand Est</idno><idno type="stamp" n="INRIA">INRIA - Institut National de Recherche en Informatique et en Automatique</idno></seriesStmt><notesStmt><note type="audience" n="2">International</note><note type="invited" n="0">No</note><note type="popular" n="0">No</note><note type="peer" n="1">Yes</note><note type="proceedings" n="1">Yes</note></notesStmt><sourceDesc><biblStruct><analytic><title xml:lang="en">A procedure for automatic proof nets construction</title><author role="aut"><persName><forename type="first">Didier</forename><surname>Galmiche</surname></persName><email>galmiche@loria.fr</email><idno type="halAuthorId">59059</idno><affiliation ref="#struct-300291"></affiliation><affiliation ref="#struct-454503"></affiliation></author><author role="aut"><persName><forename type="first">Guy</forename><surname>Perrier</surname></persName><email>perrier@loria.fr</email><idno type="idHal">guy-perrier</idno><idno type="halAuthorId">59311</idno><affiliation ref="#struct-454503"></affiliation><affiliation ref="#struct-300291"></affiliation></author></analytic><monogr><meeting><title>Conference on Logic Programming and Automated Reasoning, LPAR'92</title><date type="start">1992</date><settlement>St-Petersburg</settlement><country key="RU">Russia</country></meeting><imprint><biblScope unit="serie">LNCS</biblScope><biblScope unit="volume">624</biblScope><biblScope unit="pp">42-53</biblScope><date type="datePub">1992</date></imprint></monogr></biblStruct></sourceDesc><profileDesc><langUsage><language ident="en">English</language></langUsage><textClass><keywords scheme="author"><term xml:lang="en">Linear Logic</term><term xml:lang="en">Proof nets</term></keywords><classCode scheme="halDomain" n="info.info-cl">Computer Science [cs]/Computation and Language [cs.CL]</classCode><classCode scheme="halTypology" n="COMM">Conference papers</classCode></textClass><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.</abstract></profileDesc></hal></record>Pour manipuler ce document sous Unix (Dilib)
EXPLOR_STEP=$WICRI_ROOT/Wicri/Lorraine/explor/InforLorV4/Data/Hal/Corpus
HfdSelect -h $EXPLOR_STEP/biblio.hfd -nk 000830 | SxmlIndent | more
Ou
HfdSelect -h $EXPLOR_AREA/Data/Hal/Corpus/biblio.hfd -nk 000830 | SxmlIndent | more
Pour mettre un lien sur cette page dans le réseau Wicri
{{Explor lien
|wiki= Wicri/Lorraine
|area= InforLorV4
|flux= Hal
|étape= Corpus
|type= RBID
|clé= Hal:hal-01297750
|texte= A procedure for automatic proof nets construction
}}
| This area was generated with Dilib version V0.6.33. |  |