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).

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