Deciding Boolean BI (via Display Logic)

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

• James Brotherston, Imperial College London
• Friday 06 March 2009, 14:00-15:00
• Room FW11, Computer Laboratory, William Gates Building.

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.

This talk is included in these lists:

• All Talks (aka the CURE list)
• Cambridge talks
• Computing and Mathematics
• Department of Computer Science and Technology talks and seminars
• Interested Talks
• Logic and Semantics Seminar (Computer Laboratory)
• Room FW11, Computer Laboratory, William Gates Building
• School of Technology
• Trust & Technology Initiative - interesting events
• bld31
• yk373's list

Note that ex-directory lists are not shown.