Warning: This paper contains a mistake, rendering the proof of the main theorem invalid. 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.

翻译：[翻译摘要] 警告：本文存在一处错误，导致主要定理的证明无效。Bunched Implications（BI）逻辑同时包含加性连接词与乘性连接词，其中包含两种原始直觉主义蕴含。因此，相继式表述中的上下文既非列表也非多重集，而是称为束的树状结构。尽管存在这种额外的复杂性，该逻辑仍具有良构的元理论，可容纳所有常规形式的语义与证明系统。然而，自该逻辑诞生以来，有效的证明搜索过程一直难以实现。我们证明：可将任意给定相继式的证明搜索空间归约为原始递归集合，该论证将根岑关于经典命题逻辑的可判定性论证进行了推广，并融合了戴科夫关于直觉主义逻辑消去收缩论证的关键特征。由此推论可得到有效的证明搜索过程及可证明性的可判定性。