Proof-search and countermodel generation in propositional BI logic
Identifieur interne :
000900 ( PascalFrancis/Corpus );
précédent :
000899;
suivant :
000901
Proof-search and countermodel generation in propositional BI logic
Auteurs : Didier Galmiche ;
Daniel MerySource :
-
Lecture notes in computer science [ 0302-9743 ] ; 2001.
RBID : Pascal:02-0060254
Descripteurs français
English descriptors
Abstract
In this paper, we study proof-search in the propositional BI logic that can be viewed as a merging of intuitionistic logic and multiplicative intuitionistic linear logic. With its underlying sharing interpretation, BI has been recently used for logic programming or reasoning about mutable data structures. We propose a labelled tableau calculus for BI, the use of labels making it possible to generate countermodels. We show that, from a given formula A, a non-redundant tableau construction procedure terminates and yields either a tableau proof of A or a countermodel of A in terms of the Kripke resource monoid semantics. Moreover, we show the finite model property for BI with respect to this semantics.
Notice en format standard (ISO 2709)
Pour connaître la documentation sur le format Inist Standard.
pA |
A01 | 01 | 1 | | @0 0302-9743 |
---|
A05 | | | | @2 2215 |
---|
A08 | 01 | 1 | ENG | @1 Proof-search and countermodel generation in propositional BI logic |
---|
A09 | 01 | 1 | ENG | @1 TACS 2001 : theoretical aspects of computer software : Sendai, 29-31 October 2001 |
---|
A11 | 01 | 1 | | @1 GALMICHE (Didier) |
---|
A11 | 02 | 1 | | @1 MERY (Daniel) |
---|
A12 | 01 | 1 | | @1 KOBAYASHI (Naoki) @9 ed. |
---|
A12 | 02 | 1 | | @1 PIERCE (Benjamin C.) @9 ed. |
---|
A14 | 01 | | | @1 LORIA - Université Henri Poincaré, Campus Scientifique, BP 239 @2 54506 Vandœuvre-lès-Nancy @3 FRA @Z 1 aut. @Z 2 aut. |
---|
A20 | | | | @1 263-282 |
---|
A21 | | | | @1 2001 |
---|
A23 | 01 | | | @0 ENG |
---|
A26 | 01 | | | @0 3-540-42736-8 |
---|
A43 | 01 | | | @1 INIST @2 16343 @5 354000097033730130 |
---|
A44 | | | | @0 0000 @1 © 2002 INIST-CNRS. All rights reserved. |
---|
A45 | | | | @0 15 ref. |
---|
A47 | 01 | 1 | | @0 02-0060254 |
---|
A60 | | | | @1 P @2 C |
---|
A61 | | | | @0 A |
---|
A64 | 01 | 1 | | @0 Lecture notes in computer science |
---|
A66 | 01 | | | @0 DEU |
---|
A66 | 02 | | | @0 USA |
---|
C01 | 01 | | ENG | @0 In this paper, we study proof-search in the propositional BI logic that can be viewed as a merging of intuitionistic logic and multiplicative intuitionistic linear logic. With its underlying sharing interpretation, BI has been recently used for logic programming or reasoning about mutable data structures. We propose a labelled tableau calculus for BI, the use of labels making it possible to generate countermodels. We show that, from a given formula A, a non-redundant tableau construction procedure terminates and yields either a tableau proof of A or a countermodel of A in terms of the Kripke resource monoid semantics. Moreover, we show the finite model property for BI with respect to this semantics. |
---|
C02 | 01 | X | | @0 001D01A04 |
---|
C03 | 01 | X | FRE | @0 Programmation logique @5 16 |
---|
C03 | 01 | X | ENG | @0 Logical programming @5 16 |
---|
C03 | 01 | X | SPA | @0 Programación lógica @5 16 |
---|
C03 | 02 | X | FRE | @0 Logique propositionnelle @5 17 |
---|
C03 | 02 | X | ENG | @0 Propositional logic @5 17 |
---|
C03 | 02 | X | SPA | @0 Lógica proposicional @5 17 |
---|
C03 | 03 | X | FRE | @0 Théorie preuve @5 18 |
---|
C03 | 03 | X | ENG | @0 Proof theory @5 18 |
---|
C03 | 03 | X | SPA | @0 Teoría demonstración @5 18 |
---|
N21 | | | | @1 028 |
---|
|
pR |
A30 | 01 | 1 | ENG | @1 Theoretical aspects of computer software. International symposium @2 4 @3 Sendai JPN @4 2001-10-29 |
---|
|
Format Inist (serveur)
NO : | PASCAL 02-0060254 INIST |
ET : | Proof-search and countermodel generation in propositional BI logic |
AU : | GALMICHE (Didier); MERY (Daniel); KOBAYASHI (Naoki); PIERCE (Benjamin C.) |
AF : | LORIA - Université Henri Poincaré, Campus Scientifique, BP 239/54506 Vandœuvre-lès-Nancy/France (1 aut., 2 aut.) |
DT : | Publication en série; Congrès; Niveau analytique |
SO : | Lecture notes in computer science; ISSN 0302-9743; Allemagne; Da. 2001; Vol. 2215; Pp. 263-282; Bibl. 15 ref. |
LA : | Anglais |
EA : | In this paper, we study proof-search in the propositional BI logic that can be viewed as a merging of intuitionistic logic and multiplicative intuitionistic linear logic. With its underlying sharing interpretation, BI has been recently used for logic programming or reasoning about mutable data structures. We propose a labelled tableau calculus for BI, the use of labels making it possible to generate countermodels. We show that, from a given formula A, a non-redundant tableau construction procedure terminates and yields either a tableau proof of A or a countermodel of A in terms of the Kripke resource monoid semantics. Moreover, we show the finite model property for BI with respect to this semantics. |
CC : | 001D01A04 |
FD : | Programmation logique; Logique propositionnelle; Théorie preuve |
ED : | Logical programming; Propositional logic; Proof theory |
SD : | Programación lógica; Lógica proposicional; Teoría demonstración |
LO : | INIST-16343.354000097033730130 |
ID : | 02-0060254 |
Links to Exploration step
Pascal:02-0060254
Le document en format XML
<record><TEI><teiHeader><fileDesc><titleStmt><title xml:lang="en" level="a">Proof-search and countermodel generation in propositional BI logic</title>
<author><name sortKey="Galmiche, Didier" sort="Galmiche, Didier" uniqKey="Galmiche D" first="Didier" last="Galmiche">Didier Galmiche</name>
<affiliation><inist:fA14 i1="01"><s1>LORIA - Université Henri Poincaré, Campus Scientifique, BP 239</s1>
<s2>54506 Vandœuvre-lès-Nancy</s2>
<s3>FRA</s3>
<sZ>1 aut.</sZ>
<sZ>2 aut.</sZ>
</inist:fA14>
</affiliation>
</author>
<author><name sortKey="Mery, Daniel" sort="Mery, Daniel" uniqKey="Mery D" first="Daniel" last="Mery">Daniel Mery</name>
<affiliation><inist:fA14 i1="01"><s1>LORIA - Université Henri Poincaré, Campus Scientifique, BP 239</s1>
<s2>54506 Vandœuvre-lès-Nancy</s2>
<s3>FRA</s3>
<sZ>1 aut.</sZ>
<sZ>2 aut.</sZ>
</inist:fA14>
</affiliation>
</author>
</titleStmt>
<publicationStmt><idno type="wicri:source">INIST</idno>
<idno type="inist">02-0060254</idno>
<date when="2001">2001</date>
<idno type="stanalyst">PASCAL 02-0060254 INIST</idno>
<idno type="RBID">Pascal:02-0060254</idno>
<idno type="wicri:Area/PascalFrancis/Corpus">000900</idno>
</publicationStmt>
<sourceDesc><biblStruct><analytic><title xml:lang="en" level="a">Proof-search and countermodel generation in propositional BI logic</title>
<author><name sortKey="Galmiche, Didier" sort="Galmiche, Didier" uniqKey="Galmiche D" first="Didier" last="Galmiche">Didier Galmiche</name>
<affiliation><inist:fA14 i1="01"><s1>LORIA - Université Henri Poincaré, Campus Scientifique, BP 239</s1>
<s2>54506 Vandœuvre-lès-Nancy</s2>
<s3>FRA</s3>
<sZ>1 aut.</sZ>
<sZ>2 aut.</sZ>
</inist:fA14>
</affiliation>
</author>
<author><name sortKey="Mery, Daniel" sort="Mery, Daniel" uniqKey="Mery D" first="Daniel" last="Mery">Daniel Mery</name>
<affiliation><inist:fA14 i1="01"><s1>LORIA - Université Henri Poincaré, Campus Scientifique, BP 239</s1>
<s2>54506 Vandœuvre-lès-Nancy</s2>
<s3>FRA</s3>
<sZ>1 aut.</sZ>
<sZ>2 aut.</sZ>
</inist:fA14>
</affiliation>
</author>
</analytic>
<series><title level="j" type="main">Lecture notes in computer science</title>
<idno type="ISSN">0302-9743</idno>
<imprint><date when="2001">2001</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>Logical programming</term>
<term>Proof theory</term>
<term>Propositional logic</term>
</keywords>
<keywords scheme="Pascal" xml:lang="fr"><term>Programmation logique</term>
<term>Logique propositionnelle</term>
<term>Théorie preuve</term>
</keywords>
</textClass>
</profileDesc>
</teiHeader>
<front><div type="abstract" xml:lang="en">In this paper, we study proof-search in the propositional BI logic that can be viewed as a merging of intuitionistic logic and multiplicative intuitionistic linear logic. With its underlying sharing interpretation, BI has been recently used for logic programming or reasoning about mutable data structures. We propose a labelled tableau calculus for BI, the use of labels making it possible to generate countermodels. We show that, from a given formula A, a non-redundant tableau construction procedure terminates and yields either a tableau proof of A or a countermodel of A in terms of the Kripke resource monoid semantics. Moreover, we show the finite model property for BI with respect to this semantics.</div>
</front>
</TEI>
<inist><standard h6="B"><pA><fA01 i1="01" i2="1"><s0>0302-9743</s0>
</fA01>
<fA05><s2>2215</s2>
</fA05>
<fA08 i1="01" i2="1" l="ENG"><s1>Proof-search and countermodel generation in propositional BI logic</s1>
</fA08>
<fA09 i1="01" i2="1" l="ENG"><s1>TACS 2001 : theoretical aspects of computer software : Sendai, 29-31 October 2001</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>KOBAYASHI (Naoki)</s1>
<s9>ed.</s9>
</fA12>
<fA12 i1="02" i2="1"><s1>PIERCE (Benjamin C.)</s1>
<s9>ed.</s9>
</fA12>
<fA14 i1="01"><s1>LORIA - Université Henri Poincaré, Campus Scientifique, BP 239</s1>
<s2>54506 Vandœuvre-lès-Nancy</s2>
<s3>FRA</s3>
<sZ>1 aut.</sZ>
<sZ>2 aut.</sZ>
</fA14>
<fA20><s1>263-282</s1>
</fA20>
<fA21><s1>2001</s1>
</fA21>
<fA23 i1="01"><s0>ENG</s0>
</fA23>
<fA26 i1="01"><s0>3-540-42736-8</s0>
</fA26>
<fA43 i1="01"><s1>INIST</s1>
<s2>16343</s2>
<s5>354000097033730130</s5>
</fA43>
<fA44><s0>0000</s0>
<s1>© 2002 INIST-CNRS. All rights reserved.</s1>
</fA44>
<fA45><s0>15 ref.</s0>
</fA45>
<fA47 i1="01" i2="1"><s0>02-0060254</s0>
</fA47>
<fA60><s1>P</s1>
<s2>C</s2>
</fA60>
<fA64 i1="01" i2="1"><s0>Lecture notes in computer science</s0>
</fA64>
<fA66 i1="01"><s0>DEU</s0>
</fA66>
<fA66 i1="02"><s0>USA</s0>
</fA66>
<fC01 i1="01" l="ENG"><s0>In this paper, we study proof-search in the propositional BI logic that can be viewed as a merging of intuitionistic logic and multiplicative intuitionistic linear logic. With its underlying sharing interpretation, BI has been recently used for logic programming or reasoning about mutable data structures. We propose a labelled tableau calculus for BI, the use of labels making it possible to generate countermodels. We show that, from a given formula A, a non-redundant tableau construction procedure terminates and yields either a tableau proof of A or a countermodel of A in terms of the Kripke resource monoid semantics. Moreover, we show the finite model property for BI with respect to this semantics.</s0>
</fC01>
<fC02 i1="01" i2="X"><s0>001D01A04</s0>
</fC02>
<fC03 i1="01" i2="X" l="FRE"><s0>Programmation logique</s0>
<s5>16</s5>
</fC03>
<fC03 i1="01" i2="X" l="ENG"><s0>Logical programming</s0>
<s5>16</s5>
</fC03>
<fC03 i1="01" i2="X" l="SPA"><s0>Programación lógica</s0>
<s5>16</s5>
</fC03>
<fC03 i1="02" i2="X" l="FRE"><s0>Logique propositionnelle</s0>
<s5>17</s5>
</fC03>
<fC03 i1="02" i2="X" l="ENG"><s0>Propositional logic</s0>
<s5>17</s5>
</fC03>
<fC03 i1="02" i2="X" l="SPA"><s0>Lógica proposicional</s0>
<s5>17</s5>
</fC03>
<fC03 i1="03" i2="X" l="FRE"><s0>Théorie preuve</s0>
<s5>18</s5>
</fC03>
<fC03 i1="03" i2="X" l="ENG"><s0>Proof theory</s0>
<s5>18</s5>
</fC03>
<fC03 i1="03" i2="X" l="SPA"><s0>Teoría demonstración</s0>
<s5>18</s5>
</fC03>
<fN21><s1>028</s1>
</fN21>
</pA>
<pR><fA30 i1="01" i2="1" l="ENG"><s1>Theoretical aspects of computer software. International symposium</s1>
<s2>4</s2>
<s3>Sendai JPN</s3>
<s4>2001-10-29</s4>
</fA30>
</pR>
</standard>
<server><NO>PASCAL 02-0060254 INIST</NO>
<ET>Proof-search and countermodel generation in propositional BI logic</ET>
<AU>GALMICHE (Didier); MERY (Daniel); KOBAYASHI (Naoki); PIERCE (Benjamin C.)</AU>
<AF>LORIA - Université Henri Poincaré, Campus Scientifique, BP 239/54506 Vandœuvre-lès-Nancy/France (1 aut., 2 aut.)</AF>
<DT>Publication en série; Congrès; Niveau analytique</DT>
<SO>Lecture notes in computer science; ISSN 0302-9743; Allemagne; Da. 2001; Vol. 2215; Pp. 263-282; Bibl. 15 ref.</SO>
<LA>Anglais</LA>
<EA>In this paper, we study proof-search in the propositional BI logic that can be viewed as a merging of intuitionistic logic and multiplicative intuitionistic linear logic. With its underlying sharing interpretation, BI has been recently used for logic programming or reasoning about mutable data structures. We propose a labelled tableau calculus for BI, the use of labels making it possible to generate countermodels. We show that, from a given formula A, a non-redundant tableau construction procedure terminates and yields either a tableau proof of A or a countermodel of A in terms of the Kripke resource monoid semantics. Moreover, we show the finite model property for BI with respect to this semantics.</EA>
<CC>001D01A04</CC>
<FD>Programmation logique; Logique propositionnelle; Théorie preuve</FD>
<ED>Logical programming; Propositional logic; Proof theory</ED>
<SD>Programación lógica; Lógica proposicional; Teoría demonstración</SD>
<LO>INIST-16343.354000097033730130</LO>
<ID>02-0060254</ID>
</server>
</inist>
</record>
Pour manipuler ce document sous Unix (Dilib)
EXPLOR_STEP=$WICRI_ROOT/Wicri/Lorraine/explor/InforLorV4/Data/PascalFrancis/Corpus
HfdSelect -h $EXPLOR_STEP/biblio.hfd -nk 000900 | SxmlIndent | more
Ou
HfdSelect -h $EXPLOR_AREA/Data/PascalFrancis/Corpus/biblio.hfd -nk 000900 | SxmlIndent | more
Pour mettre un lien sur cette page dans le réseau Wicri
{{Explor lien
|wiki= Wicri/Lorraine
|area= InforLorV4
|flux= PascalFrancis
|étape= Corpus
|type= RBID
|clé= Pascal:02-0060254
|texte= Proof-search and countermodel generation in propositional BI logic
}}
| This area was generated with Dilib version V0.6.33. Data generation: Mon Jun 10 21:56:28 2019. Site generation: Fri Feb 25 15:29:27 2022 | ![](Common/icons/LogoDilib.gif) |