Proof-search and countermodel generation in propositional BI 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.