CISA organises a series of seminars by local and visiting speakers, covering a range of topics of relevance to intelligent systems and their applications. These are open to all and are usually held on Wednesdays at 14:00 in room 4.31 of the Informatics Forum. Seminars are usually 50 minutes long followed by 10 minutes of discussion. The seminars are publicised in the cisa-seminars and seminars mailing lists.
The seminar organiser is Adela Grando. If you have suggestions for speakers, or would like to give a talk, please email the seminar organiser.
Bunched logics, originating in O'Hearn and Pym's BI, are a relatively recent addition to the menagerie of substructural logics. They can be seen as the result of freely combining a standard (additive) propositional logic with a (multiplicative) linear logic. Bunched logics enjoy a Tarskian "resource" interpretation of formulas, which has very successfully been exploited to obtain logics for program analysis - most notably in the shape of separation logic, which is based upon an interpretation of resources as portions of heap memory.
In this talk, we examine bunched logic from a general proof-theoretic perspective. While there has been considerable interest in the semantics of bunched logics, their proof theory by contrast has received comparatively little attention; only BI possesses a well-behaved sequent calculus, which does not naturally extend to the other bunched logics such as BBI. We show how to obtain *display calculi* 'a la Belnap for all four principal bunched logics in a unified manner (each such logic being characterised by the strengths of its additive and multiplicative components). Each of our calculi satisfies cut-elimination and is sound and complete with respect to a Hilbert-style presentation of the corresponding bunched logic. By examining the relationship between our calculi and the BI sequent calculus, we also provide an explanation as to why well-behaved sequent calculi for the other bunched logics have been so elusive.
This talk is based upon a related paper by the speaker [1].
[1] James Brotherston. A unified display proof theory for bunched logic. Submitted, 2009. Available from http://www.doc.ic.ac.uk/~jbrother/