# Proof-search and countermodel generation in propositional BI Logic - extended abstract -

1 TYPES - Logic, proof Theory and Programming
LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications
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.
Mots-clés :
Type de document :
Communication dans un congrès
N. Kobayashi, B.C. Pierce. 4th International Symposium on Theoretical Aspects of Computer Software - TACS 2001, 2001, Sendai, Japan, Springer, 2215, pp.263-282, 2001, Lecture Notes in Computer Science
Domaine :

https://hal.inria.fr/inria-00100565
Contributeur : Publications Loria <>
Soumis le : mardi 26 septembre 2006 - 14:47:38
Dernière modification le : mardi 24 avril 2018 - 13:32:45

### Identifiants

• HAL Id : inria-00100565, version 1

### Citation

Didier Galmiche, Daniel Méry. Proof-search and countermodel generation in propositional BI Logic - extended abstract -. N. Kobayashi, B.C. Pierce. 4th International Symposium on Theoretical Aspects of Computer Software - TACS 2001, 2001, Sendai, Japan, Springer, 2215, pp.263-282, 2001, Lecture Notes in Computer Science. 〈inria-00100565〉

### Métriques

Consultations de la notice