  The logic of Bunched Implications (BI) combines both additive and
multiplicative connectives, which include two primitive intuitionistic
implications. As a consequence, contexts in the sequent presentation are not
lists, nor multisets, but rather tree-like structures called bunches. This
additional complexity notwithstanding, the logic has a well-behaved metatheory
admitting all the familiar forms of semantics and proof systems. However, the
presentation of an effective proof-search procedure has been elusive since the
logic's debut. We show that one can reduce the proof-search space for any given
sequent to a primitive recursive set, the argument generalizing Gentzen's
decidability argument for classical propositional logic and combining key
features of Dyckhoff's contraction-elimination argument for intuitionistic
logic. An effective proof-search procedure, and hence decidability of
provability, follows as a corollary.
