Naming proofs in classical propositional logic
Identifieur interne : 006613 ( Main/Merge ); précédent : 006612; suivant : 006614Naming proofs in classical propositional logic
Auteurs : Francois Lamarche [France] ; Lutz Strassburger [Allemagne]Source :
- Lecture notes in computer science [ 0302-9743 ] ; 2005.
Descripteurs français
- Pascal (Inist)
English descriptors
- KwdEn :
Abstract
We present a theory of proof denotations in classical propositional logic. The abstract definition is in terms of a semiring of weights, and two concrete instances are explored. With the Boolean semiring we get a theory of classical proof nets, with a geometric correctness criterion, a sequentialization theorem, and a strongly normalizing cut-elimination procedure. This gives us a "Boolean" category, which is not a poset. With the semiring of natural numbers, we obtain a sound semantics for classical logic, in which fewer proofs are identified. Though a "real" sequentialization theorem is missing, these proof nets have a grip on complexity issues. In both cases the cut elimination procedure is closely related to its equivalent in the calculus of structures.
Links toward previous steps (curation, corpus...)
- to stream PascalFrancis, to step Corpus: 000535
- to stream PascalFrancis, to step Curation: 000503
- to stream PascalFrancis, to step Checkpoint: 000476
Links to Exploration step
Pascal:05-0358285Le document en format XML
<record><TEI><teiHeader><fileDesc><titleStmt><title xml:lang="en" level="a">Naming proofs in classical propositional logic</title><author><name sortKey="Lamarche, Francois" sort="Lamarche, Francois" uniqKey="Lamarche F" first="Francois" last="Lamarche">Francois Lamarche</name><affiliation wicri:level="3"><inist:fA14 i1="01"><s1>LORIA & INRIA-Lorraine, Projet Calligramme, 615, rue du Jardin Botanique</s1><s2>54602 Villers-lès-Nancy</s2><s3>FRA</s3><sZ>1 aut.</sZ></inist:fA14><country>France</country><placeName><region type="region" nuts="2">Grand Est</region><region type="old region" nuts="2">Lorraine (région)</region><settlement type="city">Villers-lès-Nancy</settlement></placeName></affiliation></author><author><name sortKey="Strassburger, Lutz" sort="Strassburger, Lutz" uniqKey="Strassburger L" first="Lutz" last="Strassburger">Lutz Strassburger</name><affiliation wicri:level="3"><inist:fA14 i1="02"><s1>Universität des Saarlandes, Informatik - Programmiersysteme, Postfach 15 11 50</s1><s2>66041 Saarbrücken</s2><s3>DEU</s3><sZ>2 aut.</sZ></inist:fA14><country>Allemagne</country><placeName><region type="land" nuts="2">Sarre (Land)</region><settlement type="city">Sarrebruck</settlement></placeName></affiliation></author></titleStmt><publicationStmt><idno type="wicri:source">INIST</idno><idno type="inist">05-0358285</idno><date when="2005">2005</date><idno type="stanalyst">PASCAL 05-0358285 INIST</idno><idno type="RBID">Pascal:05-0358285</idno><idno type="wicri:Area/PascalFrancis/Corpus">000535</idno><idno type="wicri:Area/PascalFrancis/Curation">000503</idno><idno type="wicri:Area/PascalFrancis/Checkpoint">000476</idno><idno type="wicri:explorRef" wicri:stream="PascalFrancis" wicri:step="Checkpoint">000476</idno><idno type="wicri:doubleKey">0302-9743:2005:Lamarche F:naming:proofs:in</idno><idno type="wicri:Area/Main/Merge">006613</idno></publicationStmt><sourceDesc><biblStruct><analytic><title xml:lang="en" level="a">Naming proofs in classical propositional logic</title><author><name sortKey="Lamarche, Francois" sort="Lamarche, Francois" uniqKey="Lamarche F" first="Francois" last="Lamarche">Francois Lamarche</name><affiliation wicri:level="3"><inist:fA14 i1="01"><s1>LORIA & INRIA-Lorraine, Projet Calligramme, 615, rue du Jardin Botanique</s1><s2>54602 Villers-lès-Nancy</s2><s3>FRA</s3><sZ>1 aut.</sZ></inist:fA14><country>France</country><placeName><region type="region" nuts="2">Grand Est</region><region type="old region" nuts="2">Lorraine (région)</region><settlement type="city">Villers-lès-Nancy</settlement></placeName></affiliation></author><author><name sortKey="Strassburger, Lutz" sort="Strassburger, Lutz" uniqKey="Strassburger L" first="Lutz" last="Strassburger">Lutz Strassburger</name><affiliation wicri:level="3"><inist:fA14 i1="02"><s1>Universität des Saarlandes, Informatik - Programmiersysteme, Postfach 15 11 50</s1><s2>66041 Saarbrücken</s2><s3>DEU</s3><sZ>2 aut.</sZ></inist:fA14><country>Allemagne</country><placeName><region type="land" nuts="2">Sarre (Land)</region><settlement type="city">Sarrebruck</settlement></placeName></affiliation></author></analytic><series><title level="j" type="main">Lecture notes in computer science</title><idno type="ISSN">0302-9743</idno><imprint><date when="2005">2005</date></imprint></series></biblStruct></sourceDesc><seriesStmt><title level="j" type="main">Lecture notes in computer science</title><idno type="ISSN">0302-9743</idno></seriesStmt></fileDesc><profileDesc><textClass><keywords scheme="KwdEn" xml:lang="en"><term>Boolean logic</term><term>Cut elimination</term><term>Distributed system</term><term>First order logic</term><term>Lambda calculus</term><term>Naming</term><term>Partial ordering</term><term>Proof net</term><term>Proof theory</term><term>Propositional logic</term><term>Semantics</term><term>Semiring</term><term>Type theory</term></keywords><keywords scheme="Pascal" xml:lang="fr"><term>Lambda calcul</term><term>Théorie type</term><term>Logique ordre 1</term><term>Logique propositionnelle</term><term>Théorie preuve</term><term>Système réparti</term><term>Dénomination</term><term>Logique booléenne</term><term>Relation ordre partiel</term><term>Sémantique</term><term>Semianneau</term><term>Elimination coupure</term><term>Réseau preuve</term><term>.</term></keywords></textClass></profileDesc></teiHeader><front><div type="abstract" xml:lang="en">We present a theory of proof denotations in classical propositional logic. The abstract definition is in terms of a semiring of weights, and two concrete instances are explored. With the Boolean semiring we get a theory of classical proof nets, with a geometric correctness criterion, a sequentialization theorem, and a strongly normalizing cut-elimination procedure. This gives us a "Boolean" category, which is not a poset. With the semiring of natural numbers, we obtain a sound semantics for classical logic, in which fewer proofs are identified. Though a "real" sequentialization theorem is missing, these proof nets have a grip on complexity issues. In both cases the cut elimination procedure is closely related to its equivalent in the calculus of structures.</div></front></TEI><affiliations><list><country><li>Allemagne</li><li>France</li></country><region><li>Grand Est</li><li>Lorraine (région)</li><li>Sarre (Land)</li></region><settlement><li>Sarrebruck</li><li>Villers-lès-Nancy</li></settlement></list><tree><country name="France"><region name="Grand Est"><name sortKey="Lamarche, Francois" sort="Lamarche, Francois" uniqKey="Lamarche F" first="Francois" last="Lamarche">Francois Lamarche</name></region></country><country name="Allemagne"><region name="Sarre (Land)"><name sortKey="Strassburger, Lutz" sort="Strassburger, Lutz" uniqKey="Strassburger L" first="Lutz" last="Strassburger">Lutz Strassburger</name></region></country></tree></affiliations></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 006613 | SxmlIndent | more
Ou
HfdSelect -h $EXPLOR_AREA/Data/Main/Merge/biblio.hfd -nk 006613 | 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é= Pascal:05-0358285
|texte= Naming proofs in classical propositional logic
}}
| This area was generated with Dilib version V0.6.33. |  |