University of Cambridge > > Logic and Semantics Seminar (Computer Laboratory) > Deciding Boolean BI (via Display Logic)

Deciding Boolean BI (via Display Logic)

Add to your list(s) Download to your calendar using vCal

If you have a question about this talk, please contact Tom Ridge.

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 .

This talk is part of the Logic and Semantics Seminar (Computer Laboratory) series.

Tell a friend about this talk:

This talk is included in these lists:

Note that ex-directory lists are not shown.


© 2006-2024, University of Cambridge. Contact Us | Help and Documentation | Privacy and Publicity