InforLorV4, PascalFrancis, Corpus, bibRecord, 000900

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 Mery

Source :

Lecture notes in computer science [ 0302-9743 ] ; 2001.

RBID : Pascal:02-0060254

Descripteurs français

Pascal (Inist)
- Programmation logique, Logique propositionnelle, Théorie preuve.

English descriptors

KwdEn :
- Logical programming, Proof theory, Propositional logic.

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.

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`

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>
<fA61><s0>A</s0>
</fA61>
<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

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

	Serveur d'exploration sur la recherche en informatique en Lorraine
	Attention, ce site est en cours de développement ! Attention, site généré par des moyens informatiques à partir de corpus bruts. Les informations ne sont donc pas validées.

Serveur d'exploration sur la recherche en informatique en Lorraine

Proof-search and countermodel generation in propositional BI logic

Proof-search and countermodel generation in propositional BI logic

Source :

Descripteurs français

English descriptors

Abstract

Notice en format standard (ISO 2709)

Format Inist (serveur)

Links to Exploration step

Le document en format XML

Pour manipuler ce document sous Unix (Dilib)

Pour mettre un lien sur cette page dans le réseau Wicri