Linear logic (LL) is a resource-aware, abstract logic programming language that refines both classical and intuitionistic logic. Linear logic semantics is typically presented in one of two ways: by associating each formula with the set of all contexts that can be used to prove it (e.g. phase semantics) or by assigning meaning directly to proofs (e.g. coherence spaces). This work proposes a different perspective on assigning meaning to proofs by adopting a proof-theoretic perspective. More specifically, we employ base-extension semantics (BeS) to characterise proofs through the notion of base support. Recent developments have shown that BeS is powerful enough to capture proof-theoretic notions in structurally rich logics such as intuitionistic linear logic. In this paper, we extend this framework to the classical case, presenting a proof-theoretic approach to the semantics of the multiplicative-additive fragment of linear logic (MALL).

翻译：线性逻辑（LL）是一种资源敏感的逻辑编程语言，它同时细化了经典逻辑和直觉主义逻辑。线性逻辑的语义通常以两种方式呈现：一是将每个公式与所有可证明该公式的上下文集合相关联（例如相位语义），二是直接将意义赋予证明（例如相干空间语义）。本研究通过采用证明论的视角，提出了一种为证明赋予意义的不同路径。具体而言，我们运用基扩展语义（BeS），通过基支持的概念来刻画证明。近期的研究表明，BeS足够强大，能够捕捉如直觉主义线性逻辑这类结构丰富逻辑中的证明论概念。在本文中，我们将此框架扩展至经典情形，为线性逻辑的乘加片段（MALL）的语义提出了一种证明论方法。