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.

• Type: Conference
• Year: 2004
• Where: LPAR
• Authors: Kevin Donnelly, Tyler Gibson, Neel Krishnaswami, Stephen Magill, Sungwoo Park
• Keywords: Cut-free Sequent Calculi, Inverse Method, LPAR 2004, Theorem Proving Method