Semantic Labelled Tableaux for propositional BI (without bottom)
Identifieur interne : 007607 ( Main/Exploration ); précédent : 007606; suivant : 007608Semantic Labelled Tableaux for propositional BI (without bottom)
Auteurs : Didier Galmiche ; Daniel MerySource :
- Journal of Logic and Computation ; 2003.
English descriptors
- KwdEn :
Abstract
In this paper, we study semantic labelled tableaux for the propositional Bunched Implications logic (BI) that freely combines intuitionistic logic (IL) and multiplicative intuitionistic linear logic (MILL). BI is a resource-aware logic that captures interferences between resources and it is well suited, because of its resource-based sharing interpretation, for reasoning about mutable data structures. We propose a labelled tableau calculus for BI without bottom, that is the unit of the additive disjunction, based on particular labels and constraints. We prove the soundness and completeness of this calculus wrt the Kripke resource semantics with an emphasis on countermodel construction. In addition, we prove the finite model property and as a consequence the decidability. Moreover, we analyze some algorithmic aspects of the tableau construction by providing a free variable variant of the calculus. We also develop the restrictions to IL and MILL that provide new tableau methods for both logics with generation of countermodels.
Affiliations:
Links toward previous steps (curation, corpus...)
- to stream Crin, to step Corpus: 003946
- to stream Crin, to step Curation: 003946
- to stream Crin, to step Checkpoint: 000B38
- to stream Main, to step Merge: 007985
- to stream Main, to step Curation: 007607
Le document en format XML
<record><TEI><teiHeader><fileDesc><titleStmt><title xml:lang="en" wicri:score="412">Semantic Labelled Tableaux for propositional BI (without bottom)</title>
</titleStmt>
<publicationStmt><idno type="RBID">CRIN:galmiche03c</idno>
<date when="2003" year="2003">2003</date>
<idno type="wicri:Area/Crin/Corpus">003946</idno>
<idno type="wicri:Area/Crin/Curation">003946</idno>
<idno type="wicri:explorRef" wicri:stream="Crin" wicri:step="Curation">003946</idno>
<idno type="wicri:Area/Crin/Checkpoint">000B38</idno>
<idno type="wicri:explorRef" wicri:stream="Crin" wicri:step="Checkpoint">000B38</idno>
<idno type="wicri:Area/Main/Merge">007985</idno>
<idno type="wicri:Area/Main/Curation">007607</idno>
<idno type="wicri:Area/Main/Exploration">007607</idno>
</publicationStmt>
<sourceDesc><biblStruct><analytic><title xml:lang="en">Semantic Labelled Tableaux for propositional BI (without bottom)</title>
<author><name sortKey="Galmiche, Didier" sort="Galmiche, Didier" uniqKey="Galmiche D" first="Didier" last="Galmiche">Didier Galmiche</name>
</author>
<author><name sortKey="Mery, Daniel" sort="Mery, Daniel" uniqKey="Mery D" first="Daniel" last="Mery">Daniel Mery</name>
</author>
</analytic>
<series><title level="j">Journal of Logic and Computation</title>
<imprint><date when="2003" type="published">2003</date>
</imprint>
</series>
</biblStruct>
</sourceDesc>
</fileDesc>
<profileDesc><textClass><keywords scheme="KwdEn" xml:lang="en"><term>bunched implications logic</term>
<term>decidability.</term>
<term>labels</term>
<term>semantics</term>
<term>tableaux</term>
</keywords>
</textClass>
</profileDesc>
</teiHeader>
<front><div type="abstract" xml:lang="en" wicri:score="2715">In this paper, we study semantic labelled tableaux for the propositional Bunched Implications logic (BI) that freely combines intuitionistic logic (IL) and multiplicative intuitionistic linear logic (MILL). BI is a resource-aware logic that captures interferences between resources and it is well suited, because of its resource-based sharing interpretation, for reasoning about mutable data structures. We propose a labelled tableau calculus for BI without bottom, that is the unit of the additive disjunction, based on particular labels and constraints. We prove the soundness and completeness of this calculus wrt the Kripke resource semantics with an emphasis on countermodel construction. In addition, we prove the finite model property and as a consequence the decidability. Moreover, we analyze some algorithmic aspects of the tableau construction by providing a free variable variant of the calculus. We also develop the restrictions to IL and MILL that provide new tableau methods for both logics with generation of countermodels.</div>
</front>
</TEI>
<affiliations><list></list>
<tree><noCountry><name sortKey="Galmiche, Didier" sort="Galmiche, Didier" uniqKey="Galmiche D" first="Didier" last="Galmiche">Didier Galmiche</name>
<name sortKey="Mery, Daniel" sort="Mery, Daniel" uniqKey="Mery D" first="Daniel" last="Mery">Daniel Mery</name>
</noCountry>
</tree>
</affiliations>
</record>
Pour manipuler ce document sous Unix (Dilib)
EXPLOR_STEP=$WICRI_ROOT/Wicri/Lorraine/explor/InforLorV4/Data/Main/Exploration
HfdSelect -h $EXPLOR_STEP/biblio.hfd -nk 007607 | SxmlIndent | more
Ou
HfdSelect -h $EXPLOR_AREA/Data/Main/Exploration/biblio.hfd -nk 007607 | SxmlIndent | more
Pour mettre un lien sur cette page dans le réseau Wicri
{{Explor lien |wiki= Wicri/Lorraine |area= InforLorV4 |flux= Main |étape= Exploration |type= RBID |clé= CRIN:galmiche03c |texte= Semantic Labelled Tableaux for propositional BI (without bottom) }}
![]() | This area was generated with Dilib version V0.6.33. | ![]() |