Skip navigation
Skip navigation

A Labelled Sequent Calculus for BBI: Proof Theory and Proof Search

Hou, Zhe; Tiu, Alwen; Gore, Rajeev

Description

We present a labelled sequent calculus for Boolean BI (BBI), a classical variant of the logic of Bunched Implication. The calculus is simple, sound, complete, and enjoys cut-elimination. We show that all the structural rules in the calculus, i.e., those r

CollectionsANU Research Publications
Date published: 2013
Type: Conference paper
URI: http://hdl.handle.net/1885/65771
Source: TABLEAUX 2013, International Conference on Theorem Proving with Analytic Tableaux and Related Systems
DOI: 10.1007/978-3-642-40537-2_16

Download

File Description SizeFormat Image
01_Hou_A_Labelled_Sequent_Calculus_2013.pdf277.73 kBAdobe PDF    Request a copy


Items in Open Research are protected by copyright, with all rights reserved, unless otherwise indicated.

Updated:  20 July 2017/ Responsible Officer:  University Librarian/ Page Contact:  Library Systems & Web Coordinator