A syntactic proof of decidability for the logic of bunched implication BI

TL;DR

This paper provides a syntactic proof of decidability for the propositional logic of bunched implication BI, which is fundamental for reasoning about resources in separation logic, using a proof-theoretic approach.

Contribution

It offers the first syntactic proof of BI's decidability, avoiding complex semantic arguments, and introduces an implementable decision procedure.

Findings

Proves decidability of propositional BI using a syntactic method.

Provides an upper bound on the complexity of BI.

Results in an accessible proof-theoretic framework for BI.

Abstract

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.