COOKIES: By using this website you agree that we can place Google Analytics Cookies on your device for performance monitoring. |

University of Cambridge > Talks.cam > 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 - 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
- Computer Laboratory talks
- Computing and Mathematics
- 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. |
## Other listsProgram verification reading group. CLIO - CU history Society Lees Knowles Lectures : Total War : The Soviet Union and the Eastern Front in a Comparative Framework## Other talksPanel comparisons: Challenor, Ginsbourger, Nobile, Teckentrup and Beck 160 years of occupational structure: Late Imperial China and its regions Open as a Tool to Change Ecosystems Characterizing Immunogenetic Mechanisms through HIV Disease Analysis CANCELLED First year PhD student fieldwork seminar |