The logic of bunched implications (BI) can be seen as the free combination of intuitionistic propositional logic (IPL) and intuitionistic multiplicative linear logic (IMLL). We present here a base-extension semantics (B-eS) for BI in the spirit of Sandqvist's B-eS for IPL, deferring an analysis of proof-theoretic validity, in the sense of Dummett and Prawitz, to another occasion. Essential to BI's formulation in proof-theoretic terms is the concept of a `bunch' of hypotheses that is familiar from relevance logic. Bunches amount to trees whose internal vertices are labelled with either the IMLL context-former or the IPL context-former and whose leaves are labelled with propositions or units for the context-formers. This structure presents significant technical challenges in setting up a base-extension semantics for BI. Our approach starts from the B-eS for IPL and the B-eS for IMLL and provides a systematic combination. Such a combination requires that base rules carry bunched structure, and so requires a more complex notion of derivability in a base and a correspondingly richer notion of support in a base. One reason why BI is a substructural logic of interest is that the `resource interpretation' of its semantics, given in terms of sharing and separation and which gives rise to Separation Logic in the field of program verification, is quite distinct from the `number-of-uses' reading of the propositions of linear logic as resources. This resource reading of BI provides useful intuitions in the formulation of its proof-theoretic semantics. We discuss a simple example of the use of the given B-eS in security modelling.

翻译：束蕴逻辑（BI）可视为直觉主义命题逻辑（IPL）与直觉主义乘性线性逻辑（IMLL）的自由组合。本文基于Sandqvist为IPL建立的基扩展语义（B-eS）思想，为BI提出一种基扩展语义，而将Dummett与Prawitz意义上的证明论有效性分析留待后续研究。在证明论语境下表述BI的核心在于“假设束”概念——这一概念在相关逻辑中为人熟知。假设束本质上是树结构，其内部节点由IMLL语境构造子或IPL语境构造子标记，叶节点则由命题或语境构造子的单位元标记。这种结构在为BI建立基扩展语义时带来了显著的技术挑战。我们的方法始于IPL的B-eS与IMLL的B-eS，并提供了系统化的组合方案。这种组合要求基规则携带束结构，因此需要更复杂的基中可导性概念以及相应更丰富的基中支持关系概念。BI之所以成为备受关注的子结构逻辑，一个重要原因在于其语义的“资源解释”——基于共享与分离概念，并在程序验证领域催生了分离逻辑——与线性逻辑将命题视为资源的“使用次数”解读截然不同。BI的这种资源解读为其证明论语义的构建提供了有益的直觉。我们通过一个安全建模的简单示例，展示了所提B-eS的应用。