Typically, substructural logics are used in applications because of their resource interpretations, and these interpretations often refer to the celebrated number-of-uses reading of their implications. However, despite its prominence, this reading is not at all reflected in the truth-functional semantics of these logics. It is a proof-theoretic interpretation of the logic. Hence, one desires a \emph{proof-theoretic semantics} of such logics in which this reading is naturally expressed. This paper delivers such a semantics for the logic of Bunched Implications (BI), generalizing earlier work on IMLL, which is well-known as a logic of resources with numerous applications to verification and modelling. Specifically, it delivers a base-extension semantics (B-eS) for BI in which resources are \emph{bunches} of atoms that get passed from antecedent to consequent in precisely the expected way.

翻译：通常，子结构逻辑因其资源解释而被应用于实际场景，这些解释常常引用其蕴含关系著名的"使用次数"解读。然而，尽管这种解读具有重要地位，却完全未反映在这些逻辑的真值函数语义中——它本质上是一种对该逻辑的证明论解释。因此，需要为这类逻辑构建一种能自然表达该解读的\emph{证明论语义}。本文针对束蕴含逻辑（BI）建立了这样一种语义，推广了早期关于IMLL的研究成果（IMLL作为著名的资源逻辑在验证与建模领域有大量应用）。具体而言，本文为BI提供了一种基扩展语义（B-eS），其中资源是按预期方式从前件传递到后件的原子\emph{束}。