InforLorV4, Hal, Curation, bibRecord, 003697

On Proof Normalization in Linear Logic

Identifieur interne : 003697 ( Hal/Curation ); précédent : 003696; suivant : 003698

On Proof Normalization in Linear Logic

Auteurs : Didier Galmiche [France] ; Guy Perrier [France]

Source :

RBID : Hal:hal-01297755

English descriptors

mix :
- Linear Logic, Proof Theory.

Abstract

We present a proof-theoretic foundation for automated deduction in linear logic. At first, we systematically study the permutability properties of theinference rules in this logical framework and exploit these to introduce an appropriate notion of forward and backward movement of an inference in a proof. Then we discuss the naturally-arising question of the redundancy reduction and investigate the definition of the normal proof concept. We briefly consider some of the issues related to proof construction mechanization in linear logic and to the design of logic programming languages from linear logic fragments.

Url:

https://hal.inria.fr/hal-01297755

Links toward previous steps (curation, corpus...)

to stream Hal, to step Corpus: Pour aller vers cette notice dans l'étape Curation :003697

Links to Exploration step

Hal:hal-01297755

Le document en format XML

<record><TEI><teiHeader><fileDesc><titleStmt><title xml:lang="en">On Proof Normalization in Linear Logic</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-01297755</idno>
<idno type="halId">hal-01297755</idno>
<idno type="halUri">https://hal.inria.fr/hal-01297755</idno>
<idno type="url">https://hal.inria.fr/hal-01297755</idno>
<date when="1994">1994</date>
<idno type="wicri:Area/Hal/Corpus">003697</idno>
<idno type="wicri:Area/Hal/Curation">003697</idno>
</publicationStmt>
<sourceDesc><biblStruct><analytic><title xml:lang="en">On Proof Normalization in Linear Logic</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 Theory</term>
</keywords>
</textClass>
</profileDesc>
</teiHeader>
<front><div type="abstract" xml:lang="en">We present a proof-theoretic foundation for automated deduction in linear logic. At first, we systematically study the permutability properties of theinference rules in this logical framework and exploit these to introduce an appropriate notion of forward and backward movement of an inference in a proof. Then we discuss the naturally-arising question of the redundancy reduction and investigate the definition of the normal proof concept. We briefly consider some of the issues related to proof construction mechanization in linear logic and to the design of logic programming languages from linear logic fragments.</div>
</front>
</TEI>
<hal api="V3"><titleStmt><title xml:lang="en">On Proof Normalization in Linear Logic</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:42:32</date>
<date type="whenModified">2016-05-14 01:05:34</date>
<date type="whenReleased">2016-05-13 17:16:09</date>
<date type="whenProduced">1994</date>
<date type="whenEndEmbargoed">2016-04-04</date>
<ref type="file" target="https://hal.inria.fr/hal-01297755/document"><date notBefore="2016-04-04"></date>
</ref>
<ref type="file" subtype="author" n="1" target="https://hal.inria.fr/hal-01297755/file/tcs1994.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-01297755</idno>
<idno type="halUri">https://hal.inria.fr/hal-01297755</idno>
<idno type="halBibtex">galmiche:hal-01297755</idno>
<idno type="halRefHtml">Journal of Theoretical Computer Science (TCS), Elsevier, 1994, 135 (1), pp.67-110</idno>
<idno type="halRef">Journal of Theoretical Computer Science (TCS), Elsevier, 1994, 135 (1), pp.67-110</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="popular" n="0">No</note>
<note type="peer" n="1">Yes</note>
</notesStmt>
<sourceDesc><biblStruct><analytic><title xml:lang="en">On Proof Normalization in Linear Logic</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><idno type="halJournalId" status="VALID">20953</idno>
<title level="j">Journal of Theoretical Computer Science (TCS)</title>
<imprint><publisher>Elsevier</publisher>
<biblScope unit="volume">135</biblScope>
<biblScope unit="issue">1</biblScope>
<biblScope unit="pp">67-110</biblScope>
<date type="datePub">1994</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 Theory</term>
</keywords>
<classCode scheme="halDomain" n="info.info-cl">Computer Science [cs]/Computation and Language [cs.CL]</classCode>
<classCode scheme="halTypology" n="ART">Journal articles</classCode>
</textClass>
<abstract xml:lang="en">We present a proof-theoretic foundation for automated deduction in linear logic. At first, we systematically study the permutability properties of theinference rules in this logical framework and exploit these to introduce an appropriate notion of forward and backward movement of an inference in a proof. Then we discuss the naturally-arising question of the redundancy reduction and investigate the definition of the normal proof concept. We briefly consider some of the issues related to proof construction mechanization in linear logic and to the design of logic programming languages from linear logic fragments.</abstract>
</profileDesc>
</hal>
</record>

Pour manipuler ce document sous Unix (Dilib)

EXPLOR_STEP=$WICRI_ROOT/Wicri/Lorraine/explor/InforLorV4/Data/Hal/Curation

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

HfdSelect -h $EXPLOR_AREA/Data/Hal/Curation/biblio.hfd -nk 003697 | SxmlIndent | more

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

{{Explor lien
   |wiki=    Wicri/Lorraine
   |area=    InforLorV4
   |flux=    Hal
   |étape=   Curation
   |type=    RBID
   |clé=     Hal:hal-01297755
   |texte=   On Proof Normalization in Linear Logic
}}

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

On Proof Normalization in Linear Logic

On Proof Normalization in Linear Logic

Source :

English descriptors

Abstract

Links toward previous steps (curation, corpus...)

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