The logic of bunched implication BI provides a framework for reasoning about resource composition and forms the basis for an assertion language of separation logic which is used to reason about software programs. Propositional BI is obtained by freely combining propositional intuitionistic logic and multiplicative intuitionistic linear logic. It possesses an elegant proof theory: its bunched calculus combines the sequent calculi for these logics. Several natural extensions of BI have been shown as undecidable, e.g. Boolean BI which replaces intuitionistic logic with classical logic. This makes the decidability of BI, proved recently via an intricate semantical argument, particularly noteworthy. However, a syntactic proof of decidability has thus far proved elusive. We obtain such a proof here using a proof-theoretic argument. The proof is technically interesting, accessible as it uses the usual bunched calculus (it does not require any knowledge of the semantics of BI), yields an implementable decision procedure and implies an upper bound on the complexity of the logic.

翻译：束蕴逻辑BI为资源组合推理提供了一个框架，并构成了分离逻辑断言语言的基础，后者常用于软件程序的形式化验证。命题BI通过自由结合命题直觉主义逻辑与乘性直觉主义线性逻辑而获得。该逻辑具有优雅的证明理论：其束状演算融合了这两种逻辑的相继式演算系统。BI的若干自然扩展已被证明是不可判定的，例如用经典逻辑替代直觉主义逻辑的布尔BI。这使得近期通过复杂语义论证所证明的BI可判定性显得尤为突出。然而，可判定性的语法证明至今仍难以实现。本文通过证明论方法给出了这样的证明。该证明在技术上具有研究价值：仅使用标准束状演算即可理解（无需BI语义学背景），可转化为可实现的判定程序，并能推导出该逻辑复杂度的上界。