Abstract

In the logic of bunched implications BI, one can choose to interpret the additive connectives as behaving either intuitionistically or classically. Boolean BI (BBI), obtained by making the latter choice, forms the basis of separation logic and most of the related program analysis applications. Yet, in contrast to its intuitionistic counterpart, the proof theory of BBI is (to our knowledge) almost entirely absent in the literature and its decidability has hitherto been unknown.

In this talk, we give a display calculus proof system for BBI based on Belnap’s general display logic. We show that cut-elimination holds in our system and that it is sound and complete with respect to the usual notion of validity for BBI . We then demonstrate that proof search in the system can be restricted to a finitely bounded space (without loss of generality). Thus provability in our display calculus is decidable, and consequently so too is validity in BBI .