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 (
), 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
without units. We adapt the sequent calculus for
into a forward calculus. The soundness and completeness of the calculus are proved, and a canonical form for bunches is given.
Bitte loggen Sie sich ein, um Zugang zu diesem Inhalt zu erhalten