Linear logic is a substructural logic proposed as a refinement of classical and intuitionistic logics, with applications in programming languages, game semantics, and quantum physics. We present a template for Gentzen-style linear logic sequents that supports verification of logic inference rules using automatic theorem proving. Specifically, we use the Z3 Theorem Prover [8] to check targeted inference rules based on a set of inference rules that are presumed to be valid. To demonstrate the approach, we apply it to validate several derived inference rules for two different fragments of linear logic: MLL+Mix (Multiplicative Linear Logic extended with a Mix rule) and MILL (Multiplicative Intuitionistic Linear Logic).

翻译：线性逻辑是一种子结构逻辑，作为经典逻辑与直觉主义逻辑的改进而提出，应用于编程语言、博弈语义和量子物理等领域。我们提出一个Gentzen式线性逻辑矢列的模板，支持利用自动定理证明对逻辑推理规则进行验证。具体而言，我们使用Z3定理证明器[8]，基于一组被假定有效的推理规则来检查目标推理规则。为展示该方法，我们将其应用于验证两个不同线性逻辑片段中若干派生推理规则：MLL+Mix（含Mix规则的乘法线性逻辑）和MILL（乘法直觉主义线性逻辑）。