Sciweavers

Share
LPAR
2004
Springer

The Inverse Method for the Logic of Bunched Implications

9 years 1 months ago
The Inverse Method for the Logic of Bunched Implications
Abstract. The inverse method, due to Maslov, is a forward theorem proving method for cut-free sequent calculi that relies on the subformula property. The Logic of Bunched Implications (BI), due to Pym and O’Hearn, is a logic which freely combines the familiar connectives of intuitionistic logic with multiplicative linear conjunction and its adjoint implication. We present the first formulation of an inverse method for propositional BI without units. We adapt the sequent calculus for BI into a forward calculus. The soundness and completeness of the calculus are proved, and a canonical form for bunches is given.
Kevin Donnelly, Tyler Gibson, Neel Krishnaswami, S
Added 02 Jul 2010
Updated 02 Jul 2010
Type Conference
Year 2004
Where LPAR
Authors Kevin Donnelly, Tyler Gibson, Neel Krishnaswami, Stephen Magill, Sungwoo Park
Comments (0)
books