Labelled Proof Systems for Intuitionistic Provability
Identifieur interne : 002584 ( Crin/Corpus ); précédent : 002583; suivant : 002585Labelled Proof Systems for Intuitionistic Provability
Auteurs : Didier Galmiche ; Vincent BalatSource :
English descriptors
- KwdEn :
Abstract
In this paper, we propose new labelled proof systems to analyse the intuitionistic provability in classical and linear logics. An important point is to understand how search in a non-classical logic can be viewed as a perturbation of search in classical logic. Therefore, suitable characterizations of intuitionistic provability and related labelled sequent calculi are defined for linear logic. An alternative approach, based on the notion of proof-net and on the definition of suitable labelled classical proof-nets, allows to directly study the intuitionistic provability by constructing intuitionistic proof-nets for sequents of classical linear logic.
Links to Exploration step
CRIN:galmiche99hLe document en format XML
<record><TEI><teiHeader><fileDesc><titleStmt><title xml:lang="en" wicri:score="329">Labelled Proof Systems for Intuitionistic Provability</title>
</titleStmt>
<publicationStmt><idno type="RBID">CRIN:galmiche99h</idno>
<date when="1999" year="1999">1999</date>
<idno type="wicri:Area/Crin/Corpus">002584</idno>
</publicationStmt>
<sourceDesc><biblStruct><analytic><title xml:lang="en">Labelled Proof Systems for Intuitionistic Provability</title>
<author><name sortKey="Galmiche, Didier" sort="Galmiche, Didier" uniqKey="Galmiche D" first="Didier" last="Galmiche">Didier Galmiche</name>
</author>
<author><name sortKey="Balat, Vincent" sort="Balat, Vincent" uniqKey="Balat V" first="Vincent" last="Balat">Vincent Balat</name>
</author>
</analytic>
</biblStruct>
</sourceDesc>
</fileDesc>
<profileDesc><textClass><keywords scheme="KwdEn" xml:lang="en"><term>automated deduction</term>
<term>intuitionistic logic</term>
<term>labelled sequent calculus</term>
<term>linear logic</term>
<term>proof nets</term>
<term>proof theory</term>
</keywords>
</textClass>
</profileDesc>
</teiHeader>
<front><div type="abstract" xml:lang="en" wicri:score="3527">In this paper, we propose new labelled proof systems to analyse the intuitionistic provability in classical and linear logics. An important point is to understand how search in a non-classical logic can be viewed as a perturbation of search in classical logic. Therefore, suitable characterizations of intuitionistic provability and related labelled sequent calculi are defined for linear logic. An alternative approach, based on the notion of proof-net and on the definition of suitable labelled classical proof-nets, allows to directly study the intuitionistic provability by constructing intuitionistic proof-nets for sequents of classical linear logic.</div>
</front>
</TEI>
<BibTex type="incollection"><ref>galmiche99h</ref>
<crinnumber>99-R-119</crinnumber>
<category>11</category>
<equipe>TYPES</equipe>
<author><e>Galmiche, Didier</e>
<e>Balat, Vincent</e>
</author>
<title>Labelled Proof Systems for Intuitionistic Provability</title>
<booktitle>{Labelled Deduction}</booktitle>
<publisher>Kluwer Academic Publishers</publisher>
<year>1999</year>
<volume>17</volume>
<series>Applied Logic Series</series>
<note>To appear</note>
<keywords><e>proof theory</e>
<e>intuitionistic logic</e>
<e>linear logic</e>
<e>labelled sequent calculus</e>
<e>proof nets</e>
<e>automated deduction</e>
</keywords>
<abstract>In this paper, we propose new labelled proof systems to analyse the intuitionistic provability in classical and linear logics. An important point is to understand how search in a non-classical logic can be viewed as a perturbation of search in classical logic. Therefore, suitable characterizations of intuitionistic provability and related labelled sequent calculi are defined for linear logic. An alternative approach, based on the notion of proof-net and on the definition of suitable labelled classical proof-nets, allows to directly study the intuitionistic provability by constructing intuitionistic proof-nets for sequents of classical linear logic.</abstract>
</BibTex>
</record>
Pour manipuler ce document sous Unix (Dilib)
EXPLOR_STEP=$WICRI_ROOT/Wicri/Lorraine/explor/InforLorV4/Data/Crin/Corpus
HfdSelect -h $EXPLOR_STEP/biblio.hfd -nk 002584 | SxmlIndent | more
Ou
HfdSelect -h $EXPLOR_AREA/Data/Crin/Corpus/biblio.hfd -nk 002584 | SxmlIndent | more
Pour mettre un lien sur cette page dans le réseau Wicri
{{Explor lien |wiki= Wicri/Lorraine |area= InforLorV4 |flux= Crin |étape= Corpus |type= RBID |clé= CRIN:galmiche99h |texte= Labelled Proof Systems for Intuitionistic Provability }}
![]() | This area was generated with Dilib version V0.6.33. | ![]() |