A Connection-based Characterization of Bi-intuitionistic Validity
Identifieur interne : 000081 ( PascalFrancis/Checkpoint ); précédent : 000080; suivant : 000082A Connection-based Characterization of Bi-intuitionistic Validity
Auteurs : Didier Galmiche [France] ; Daniel Mery [France]Source :
- Journal of automated reasoning [ 0168-7433 ] ; 2013.
Descripteurs français
- Pascal (Inist)
English descriptors
- KwdEn :
Abstract
We give a connection-based characterization of validity in propositional bi-intuitionistic logic in terms of specific directed graphs called R-graphs. Such a characterization is well-suited for deriving labelled proof-systems with counter-model construction facilities. We first define the notion of bi-intuitionistic R-graphs from which we then obtain a connection-based characterization of propositional bi-intuitionistic validity and derive a sound and complete cut-free free-variable labelled sequent calculus that enjoys variable splitting.
Affiliations:
Links toward previous steps (curation, corpus...)
Links to Exploration step
Pascal:14-0018676Le document en format XML
<record><TEI><teiHeader><fileDesc><titleStmt><title xml:lang="en" level="a">A Connection-based Characterization of Bi-intuitionistic Validity</title><author><name sortKey="Galmiche, Didier" sort="Galmiche, Didier" uniqKey="Galmiche D" first="Didier" last="Galmiche">Didier Galmiche</name><affiliation wicri:level="3"><inist:fA14 i1="01"><s1>Université de Lorraine - LORIA, Campus Scientifique BP 239</s1><s2>Vandœuvre-lès-Nancy</s2><s3>FRA</s3><sZ>1 aut.</sZ><sZ>2 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">Vandœuvre-lès-Nancy</settlement><settlement type="city" wicri:auto="agglo">Nancy</settlement></placeName></affiliation></author><author><name sortKey="Mery, Daniel" sort="Mery, Daniel" uniqKey="Mery D" first="Daniel" last="Mery">Daniel Mery</name><affiliation wicri:level="3"><inist:fA14 i1="01"><s1>Université de Lorraine - LORIA, Campus Scientifique BP 239</s1><s2>Vandœuvre-lès-Nancy</s2><s3>FRA</s3><sZ>1 aut.</sZ><sZ>2 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">Vandœuvre-lès-Nancy</settlement><settlement type="city" wicri:auto="agglo">Nancy</settlement></placeName></affiliation></author></titleStmt><publicationStmt><idno type="wicri:source">INIST</idno><idno type="inist">14-0018676</idno><date when="2013">2013</date><idno type="stanalyst">PASCAL 14-0018676 INIST</idno><idno type="RBID">Pascal:14-0018676</idno><idno type="wicri:Area/PascalFrancis/Corpus">000035</idno><idno type="wicri:Area/PascalFrancis/Curation">000962</idno><idno type="wicri:Area/PascalFrancis/Checkpoint">000081</idno><idno type="wicri:explorRef" wicri:stream="PascalFrancis" wicri:step="Checkpoint">000081</idno></publicationStmt><sourceDesc><biblStruct><analytic><title xml:lang="en" level="a">A Connection-based Characterization of Bi-intuitionistic Validity</title><author><name sortKey="Galmiche, Didier" sort="Galmiche, Didier" uniqKey="Galmiche D" first="Didier" last="Galmiche">Didier Galmiche</name><affiliation wicri:level="3"><inist:fA14 i1="01"><s1>Université de Lorraine - LORIA, Campus Scientifique BP 239</s1><s2>Vandœuvre-lès-Nancy</s2><s3>FRA</s3><sZ>1 aut.</sZ><sZ>2 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">Vandœuvre-lès-Nancy</settlement><settlement type="city" wicri:auto="agglo">Nancy</settlement></placeName></affiliation></author><author><name sortKey="Mery, Daniel" sort="Mery, Daniel" uniqKey="Mery D" first="Daniel" last="Mery">Daniel Mery</name><affiliation wicri:level="3"><inist:fA14 i1="01"><s1>Université de Lorraine - LORIA, Campus Scientifique BP 239</s1><s2>Vandœuvre-lès-Nancy</s2><s3>FRA</s3><sZ>1 aut.</sZ><sZ>2 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">Vandœuvre-lès-Nancy</settlement><settlement type="city" wicri:auto="agglo">Nancy</settlement></placeName></affiliation></author></analytic><series><title level="j" type="main">Journal of automated reasoning</title><title level="j" type="abbreviated">J. autom. reason.</title><idno type="ISSN">0168-7433</idno><imprint><date when="2013">2013</date></imprint></series></biblStruct></sourceDesc><seriesStmt><title level="j" type="main">Journal of automated reasoning</title><title level="j" type="abbreviated">J. autom. reason.</title><idno type="ISSN">0168-7433</idno></seriesStmt></fileDesc><profileDesc><textClass><keywords scheme="KwdEn" xml:lang="en"><term>Digraph</term><term>Directed graph</term><term>Graph theory</term><term>Intuitionistic logic</term><term>Modeling</term><term>Multigraph</term><term>Program verification</term><term>Proof theory</term><term>Propositional logic</term><term>Sequent calculus</term><term>Tree(graph)</term></keywords><keywords scheme="Pascal" xml:lang="fr"><term>Logique propositionnelle</term><term>Logique intuitionniste</term><term>Multigraphe</term><term>Théorie preuve</term><term>Vérification programme</term><term>Théorie graphe</term><term>Graphe orienté</term><term>Digraphe</term><term>Arbre graphe</term><term>Modélisation</term><term>Calcul séquent</term></keywords></textClass></profileDesc></teiHeader><front><div type="abstract" xml:lang="en">We give a connection-based characterization of validity in propositional bi-intuitionistic logic in terms of specific directed graphs called R-graphs. Such a characterization is well-suited for deriving labelled proof-systems with counter-model construction facilities. We first define the notion of bi-intuitionistic R-graphs from which we then obtain a connection-based characterization of propositional bi-intuitionistic validity and derive a sound and complete cut-free free-variable labelled sequent calculus that enjoys variable splitting.</div></front></TEI><inist><standard h6="B"><pA><fA01 i1="01" i2="1"><s0>0168-7433</s0></fA01><fA03 i2="1"><s0>J. autom. reason.</s0></fA03><fA05><s2>51</s2></fA05><fA06><s2>1</s2></fA06><fA08 i1="01" i2="1" l="ENG"><s1>A Connection-based Characterization of Bi-intuitionistic Validity</s1></fA08><fA09 i1="01" i2="1" l="ENG"><s1>Special Issue on Selected Extended Papers of CADE-23</s1></fA09><fA11 i1="01" i2="1"><s1>GALMICHE (Didier)</s1></fA11><fA11 i1="02" i2="1"><s1>MERY (Daniel)</s1></fA11><fA12 i1="01" i2="1"><s1>BJORNER (Nikolaj)</s1><s9>ed.</s9></fA12><fA12 i1="02" i2="1"><s1>SOFRONIC-STOKKERMANS (Viorica)</s1><s9>ed.</s9></fA12><fA14 i1="01"><s1>Université de Lorraine - LORIA, Campus Scientifique BP 239</s1><s2>Vandœuvre-lès-Nancy</s2><s3>FRA</s3><sZ>1 aut.</sZ><sZ>2 aut.</sZ></fA14><fA15 i1="01"><s1>Microsoft Research</s1><s2>Redmond, WA 98052</s2><s3>USA</s3><sZ>1 aut.</sZ></fA15><fA15 i1="02"><s1>Universität Koblenz-Landau, Universitätsstr. 1</s1><s2>56070 Koblenz</s2><s3>DEU</s3><sZ>2 aut.</sZ></fA15><fA15 i1="03"><s1>Max-Planck-Institut für Informatik</s1><s2>66123 Saarbrücken</s2><s3>DEU</s3><sZ>2 aut.</sZ></fA15><fA20><s1>3-26</s1></fA20><fA21><s1>2013</s1></fA21><fA23 i1="01"><s0>ENG</s0></fA23><fA43 i1="01"><s1>INIST</s1><s2>28307</s2><s5>354000505168070010</s5></fA43><fA44><s0>0000</s0><s1>© 2014 INIST-CNRS. All rights reserved.</s1></fA44><fA45><s0>14 ref.</s0></fA45><fA47 i1="01" i2="1"><s0>14-0018676</s0></fA47><fA60><s1>P</s1></fA60><fA61><s0>A</s0></fA61><fA64 i1="01" i2="1"><s0>Journal of automated reasoning</s0></fA64><fA66 i1="01"><s0>DEU</s0></fA66><fC01 i1="01" l="ENG"><s0>We give a connection-based characterization of validity in propositional bi-intuitionistic logic in terms of specific directed graphs called R-graphs. Such a characterization is well-suited for deriving labelled proof-systems with counter-model construction facilities. We first define the notion of bi-intuitionistic R-graphs from which we then obtain a connection-based characterization of propositional bi-intuitionistic validity and derive a sound and complete cut-free free-variable labelled sequent calculus that enjoys variable splitting.</s0></fC01><fC02 i1="01" i2="X"><s0>001D02A04</s0></fC02><fC03 i1="01" i2="X" l="FRE"><s0>Logique propositionnelle</s0><s5>06</s5></fC03><fC03 i1="01" i2="X" l="ENG"><s0>Propositional logic</s0><s5>06</s5></fC03><fC03 i1="01" i2="X" l="SPA"><s0>Lógica proposicional</s0><s5>06</s5></fC03><fC03 i1="02" i2="X" l="FRE"><s0>Logique intuitionniste</s0><s5>07</s5></fC03><fC03 i1="02" i2="X" l="ENG"><s0>Intuitionistic logic</s0><s5>07</s5></fC03><fC03 i1="02" i2="X" l="SPA"><s0>Lógica intuicionista</s0><s5>07</s5></fC03><fC03 i1="03" i2="X" l="FRE"><s0>Multigraphe</s0><s5>08</s5></fC03><fC03 i1="03" i2="X" l="ENG"><s0>Multigraph</s0><s5>08</s5></fC03><fC03 i1="03" i2="X" l="SPA"><s0>Multígrafo</s0><s5>08</s5></fC03><fC03 i1="04" i2="X" l="FRE"><s0>Théorie preuve</s0><s5>09</s5></fC03><fC03 i1="04" i2="X" l="ENG"><s0>Proof theory</s0><s5>09</s5></fC03><fC03 i1="04" i2="X" l="SPA"><s0>Teoría demonstración</s0><s5>09</s5></fC03><fC03 i1="05" i2="X" l="FRE"><s0>Vérification programme</s0><s5>10</s5></fC03><fC03 i1="05" i2="X" l="ENG"><s0>Program verification</s0><s5>10</s5></fC03><fC03 i1="05" i2="X" l="SPA"><s0>Verificación programa</s0><s5>10</s5></fC03><fC03 i1="06" i2="X" l="FRE"><s0>Théorie graphe</s0><s5>11</s5></fC03><fC03 i1="06" i2="X" l="ENG"><s0>Graph theory</s0><s5>11</s5></fC03><fC03 i1="06" i2="X" l="SPA"><s0>Teoría grafo</s0><s5>11</s5></fC03><fC03 i1="07" i2="X" l="FRE"><s0>Graphe orienté</s0><s5>23</s5></fC03><fC03 i1="07" i2="X" l="ENG"><s0>Directed graph</s0><s5>23</s5></fC03><fC03 i1="07" i2="X" l="SPA"><s0>Grafo orientado</s0><s5>23</s5></fC03><fC03 i1="08" i2="X" l="FRE"><s0>Digraphe</s0><s5>24</s5></fC03><fC03 i1="08" i2="X" l="ENG"><s0>Digraph</s0><s5>24</s5></fC03><fC03 i1="08" i2="X" l="SPA"><s0>Digrafo</s0><s5>24</s5></fC03><fC03 i1="09" i2="X" l="FRE"><s0>Arbre graphe</s0><s5>25</s5></fC03><fC03 i1="09" i2="X" l="ENG"><s0>Tree(graph)</s0><s5>25</s5></fC03><fC03 i1="09" i2="X" l="SPA"><s0>Arbol grafo</s0><s5>25</s5></fC03><fC03 i1="10" i2="X" l="FRE"><s0>Modélisation</s0><s5>26</s5></fC03><fC03 i1="10" i2="X" l="ENG"><s0>Modeling</s0><s5>26</s5></fC03><fC03 i1="10" i2="X" l="SPA"><s0>Modelización</s0><s5>26</s5></fC03><fC03 i1="11" i2="X" l="FRE"><s0>Calcul séquent</s0><s5>27</s5></fC03><fC03 i1="11" i2="X" l="ENG"><s0>Sequent calculus</s0><s5>27</s5></fC03><fC03 i1="11" i2="X" l="SPA"><s0>Càlculo sequente</s0><s5>27</s5></fC03><fN21><s1>020</s1></fN21><fN44 i1="01"><s1>OTO</s1></fN44><fN82><s1>OTO</s1></fN82></pA></standard></inist><affiliations><list><country><li>France</li></country><region><li>Grand Est</li><li>Lorraine (région)</li></region><settlement><li>Nancy</li><li>Vandœuvre-lès-Nancy</li></settlement></list><tree><country name="France"><region name="Grand Est"><name sortKey="Galmiche, Didier" sort="Galmiche, Didier" uniqKey="Galmiche D" first="Didier" last="Galmiche">Didier Galmiche</name></region><name sortKey="Mery, Daniel" sort="Mery, Daniel" uniqKey="Mery D" first="Daniel" last="Mery">Daniel Mery</name></country></tree></affiliations></record>Pour manipuler ce document sous Unix (Dilib)
EXPLOR_STEP=$WICRI_ROOT/Wicri/Lorraine/explor/InforLorV4/Data/PascalFrancis/Checkpoint
HfdSelect -h $EXPLOR_STEP/biblio.hfd -nk 000081 | SxmlIndent | more
Ou
HfdSelect -h $EXPLOR_AREA/Data/PascalFrancis/Checkpoint/biblio.hfd -nk 000081 | SxmlIndent | more
Pour mettre un lien sur cette page dans le réseau Wicri
{{Explor lien
|wiki= Wicri/Lorraine
|area= InforLorV4
|flux= PascalFrancis
|étape= Checkpoint
|type= RBID
|clé= Pascal:14-0018676
|texte= A Connection-based Characterization of Bi-intuitionistic Validity
}}
| This area was generated with Dilib version V0.6.33. |  |