A Unified Display Proof Theory for Bunched Logic

We formulate a unified display calculus proof theory for the four principal varieties of bunched logic by combining display calculi for their component logics. Our calculi satisfy cut-elimination, and are sound and complete with respect to their standard presentations. We show that the standard sequent calculus for BI can be seen as a reformulation of its display calculus, and argue that analogous sequent calculi for the other varieties of bunched logic seem very unlikely to exist.

• Type: Journal
• Year: 2010
• Where: ENTCS
• Authors: James Brotherston
• Keywords: Analogous Sequent Calculi, Bunched Logic, ENTCS 2010, Standard Sequent Calculus