On Proof Normalization in Linear Logic
Identifieur interne : 00D822 ( Main/Merge ); précédent : 00D821; suivant : 00D823On Proof Normalization in Linear Logic
Auteurs : D. Galmiche ; G. PerrierSource :
Abstract
We present a proof-theoretic foundation for automated deduction in linear logic. At first, we systematically study the permutability properties of the inference 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.
Links toward previous steps (curation, corpus...)
- to stream Crin, to step Corpus: 001081
- to stream Crin, to step Curation: 001081
- to stream Crin, to step Checkpoint: 003350
Links to Exploration step
CRIN:galmiche93aLe document en format XML
<record><TEI><teiHeader><fileDesc><titleStmt><title xml:lang="en" wicri:score="441">On Proof Normalization in Linear Logic</title></titleStmt><publicationStmt><idno type="RBID">CRIN:galmiche93a</idno><date when="1993" year="1993">1993</date><idno type="wicri:Area/Crin/Corpus">001081</idno><idno type="wicri:Area/Crin/Curation">001081</idno><idno type="wicri:explorRef" wicri:stream="Crin" wicri:step="Curation">001081</idno><idno type="wicri:Area/Crin/Checkpoint">003350</idno><idno type="wicri:explorRef" wicri:stream="Crin" wicri:step="Checkpoint">003350</idno><idno type="wicri:Area/Main/Merge">00D822</idno></publicationStmt><sourceDesc><biblStruct><analytic><title xml:lang="en">On Proof Normalization in Linear Logic</title><author><name sortKey="Galmiche, D" sort="Galmiche, D" uniqKey="Galmiche D" first="D." last="Galmiche">D. Galmiche</name></author><author><name sortKey="Perrier, G" sort="Perrier, G" uniqKey="Perrier G" first="G." last="Perrier">G. Perrier</name></author></analytic></biblStruct></sourceDesc></fileDesc><profileDesc><textClass></textClass></profileDesc></teiHeader><front><div type="abstract" xml:lang="en" wicri:score="2774">We present a proof-theoretic foundation for automated deduction in linear logic. At first, we systematically study the permutability properties of the inference 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></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 00D822 | SxmlIndent | more
Ou
HfdSelect -h $EXPLOR_AREA/Data/Main/Merge/biblio.hfd -nk 00D822 | 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é= CRIN:galmiche93a
|texte= On Proof Normalization in Linear Logic
}}
| This area was generated with Dilib version V0.6.33. |  |