Skip Navigation

Journal of Logic and Computation 2003 13(5):707-753; doi:10.1093/logcom/13.5.707
© 2003 by Oxford University Press
This Article
Right arrow Full Text (PDF)
Right arrow Alert me when this article is cited
Right arrow Alert me if a correction is posted
Services
Right arrow Email this article to a friend
Right arrow Similar articles in this journal
Right arrow Similar articles in ISI Web of Science
Right arrow Alert me to new issues of the journal
Right arrow Add to My Personal Archive
Right arrow Download to citation manager
Right arrow Search for citing articles in:
ISI Web of Science (2)
Right arrowRequest Permissions
Google Scholar
Right arrow Articles by Galmiche, D.
Right arrow Articles by Méry, D.
Right arrow Search for Related Content
Social Bookmarking
Add to CiteULike   Add to Connotea   Add to Del.icio.us  
What's this?

Original Article

Semantic Labelled Tableaux for Propositional BI{bot}

Didier Galmiche1 and Daniel Méry1

1 LORIA - Université Henri Poincaré, Campus Scientifique, BP 239, Vandoeuvre-lès-Nancy, France. E-mail: galmiche{at}loria.fr, dmery{at}loria.fr

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{bot}1 based on particular labels and constraints. We prove the soundness and completeness of this calculus w.r.t. the Kripke resource semantics with emphasis on countermodel construction. In addition, we prove the finite model property and as a consequence the decidability of BI{bot}. Moreover, we analyse 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.

Keywords: BI logic, intuitionistic logic, tableau method, labelled deduction, semantics.

Received 5 February 2002.


Add to CiteULike CiteULike   Add to Connotea Connotea   Add to Del.icio.us Del.icio.us    What's this?


This article has been cited by other articles:


Home page
 J Logic ComputationHome page
N. Biri and D. Galmiche
Models and Separation Logics for Resource Trees
J Logic Computation, August 1, 2007; 17(4): 687 - 726.
[Abstract] [Full Text] [PDF]


Disclaimer:
Please note that abstracts for content published before 1996 were created through digital scanning and may therefore not exactly replicate the text of the original print issues. All efforts have been made to ensure accuracy, but the Publisher will not be held responsible for any remaining inaccuracies. If you require any further clarification, please contact our Customer Services Department.