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）语义的证明论方法。