Topological Observations on Multiplicative Additive Linear Logic
作为一种尝试，以揭示的拓扑性质的组合策略的游戏语义，我们提出了一个“拓扑”的游戏乘加线性逻辑没有命题变量，包括削减移动。我们重铸的概念（获胜）的战略和削减消除在这种情况下的问题，并证明削减消除定理。最后，我们证明了可靠性和完备性。拓扑结构起着至关重要的作用，特别是通过策略形成一个层的事实。
2008-07-14 cs.LO
Games and Full Completeness for Multiplicative Linear Logic
我们提出了一个游戏语义的线性逻辑，其中公式表示游戏和证明表示获胜的策略。我们表明，我们的语义产生一个范畴模型的线性逻辑和证明完全完备的乘法线性逻辑与MIX规则：每一个获胜的策略是一个独特的无割证明网的表示。{ \em history-free}策略的概念扮演了一个关键的角色;在无历史策略和交互作用几何之间建立了强有力的联系。我们的语义学结合了极性的自然概念，导致了添加剂的精细处理。我们与Joyal，Blass等人的相关工作进行了比较。
2013-11-23 cs.LO
Logic Programming with Multiplicative Structures
本文研究纯乘法片段下基于证明网构造的逻辑编程框架，展示如何仅用资源保持且上下文无关的广义乘法操作实现上下文敏感方法，并证明部分方法超出线性逻辑MLL片段。
2024-10-01 cs.LO
Type Isomorphisms for Multiplicative-Additive Linear Logic
本文研究了乘法-加法线性逻辑中的类型同构，通过扩展结果到完整MALL，揭示了分配律和消去律等更丰富的等式理论。
2025-11-20 cs.LO
Elimination and cut-elimination in multiplicative linear logic
我们将乘法线性逻辑中的每个证明结构与一个理想相关联，该理想将证明的逻辑内容表示为多项式方程。我们展示了如何削减消除乘法证明网对应的Buchberger算法的实例计算Gröbner基地消除理论。
2022-07-22 cs.LO math.LO
On Multiplicative Linear Logic, Modality and Quantum Circuits
一个逻辑系统，来自线性逻辑和称为QMLL的介绍，并显示能够捕获所有的酉量子电路。相反，任何证明都表明通过具体的GoI解释计算一些量子电路。通过赋予乘性线性逻辑以量子模态，得到了具有割消的系统QMLL。
2012-10-02 cs.LO quant-ph
Constructing Fully Complete Models of Multiplicative Linear Logic
线性逻辑的乘法片段是这个家族中具有最好理解的证明理论的形式系统，并且最好地捕获这个理论的范畴模型是完全完备的。我们演示了如何Hyland-Tan双胶合结构产生这样的类别，无论是有或没有单位，当应用到任何一个大家庭的退化模型。这个过程解释了一些特殊情况下，这样的模型从文献。为了实现这一结果，我们开发了一个张量演算的紧闭范畴有限的双产品。我们展示了如何获得一个完全完整的模型所需的组合属性，通过这种胶合结构添加到结构已经从原来的类别。
2015-09-02 cs.LO
Stellar Resolution: Multiplicatives
我们提出了一个新的异步计算模型命名为恒星分辨率的基础上一阶统一。这个模型的计算是作为一个正式的吉拉德的先验语法程序，勾画了一系列的三篇文章。因此，这是第一步，以适当的正式处理吉拉德的建议，以解决一阶逻辑的证明程序的方法。在建立了恒星分辨率的形式定义和基本性质之后，我们解释了它是如何推广传统的计算模型的，例如逻辑编程和组合模型，例如Wang tilings。然后，我们解释它如何可以表示乘法证明结构，其削减消除和Danos和Regnier的正确性标准。可实现性技术的进一步使用导致乘法线性逻辑的动态语义，遵循先前的交互几何模型。
2020-07-31 cs.LO
Multiplicative-Additive Proof Equivalence is Logspace-complete, via Binary Decision Trees
给定一个逻辑中提出的微积分，一个自然的问题是证明的等价性：以确定是否两个给定的证明是等同的任何指称语义，即任何类别的解释逻辑兼容其削减消除程序。这个概念通常可以通过一组规则排列在语法上捕获。非常一般地，证明网可以被定义为提供证明的等价类的规范表示的组合对象。特别地，逻辑的证明网的存在性提供了该逻辑的等价性问题的解决方案。在线性逻辑的某些片段中，可以给出具有良好计算性质的证明网的概念，使其成为研究割消过程的证明的合适表示。最近已经证明，对于线性逻辑的乘法（有单位）片段，不可能有这样一个证明网的概念，因为这个逻辑的等价问题是P空间完全的。研究线性逻辑中的乘加（无单位）片段，发现它与二进制决策树密切相关：建立了基于二进制决策树的证明表示，将证明等价约化为决策树等价，并给出了二进制决策树的逆编码作为证明.作为我们的主要结果，我们得到的证明等价问题的研究片段的复杂性是对数空间完全的。
2017-11-28 cs.LO
Proof Diagrams for Multiplicative Linear Logic: Syntax and Semantics
证明网是线性逻辑证明的一种语法，它给出了关于语法相等的证明等价的粗略概念以及证明的直观几何表示。本文给出了乘法线性逻辑导子的另一种$2$维语法。字符串图的语法授权定义一个框架，其中一个术语的序列化，即决定该术语是否对应于正确的推导，可以在线性时间内验证。此外，我们可以使用这种语法来定义一个指称语义的乘法线性逻辑单元的证明图模的等价类的终止重写。
2017-02-01 cs.LO math.CT
An application of parallel cut elimination in multiplicative linear logic to the Taylor expansion of proof nets
本文研究MLL证明网并行消去的组合性质，通过路径约束保证无限加权和归约的有限性，并证明该约束适用于MELL泰勒展开中的微分网，为线性逻辑定量语义提供充分条件。
2021-12-17 cs.LO
Relational type-checking for MELL proof-structures. Part 1: Multiplicatives
线性逻辑的关系语义是一种非幂等交类型系统，从它可以恢复关于证明结构执行的若干信息。因此，具有结论$Γ$的证明结构R的关系解释的元素充当具有R作为居住者的类型（精化$Γ$）。我们感兴趣的是下面的类型检查问题：给定一个证明结构R，一个公式列表$Γ$，以及$Γ$的关系解释中的一个点x，x在R的解释中吗？这个问题是可以决定的。我们在这里提出了一个算法，决定它在时间上线性的大小R，如果R是一个证明结构的乘法片段的线性逻辑。该算法可以推广到包含$λ$ -演算的乘指数线性逻辑的更大片段。
2016-06-01 cs.LO
Proof-theoretic Semantics for Intuitionistic Multiplicative Linear Logic (Extended Abstract)
本文首次探索子结构逻辑的证明论语义，提出直觉主义乘法线性逻辑（IMLL）的基础扩展语义，其中逻辑常量定义均采用消去规则形式，并证明了其可靠性与完备性。
2024-11-12 cs.LO math.LO
A Real-Valued Modal Logic
本文提出一种实值多值模态逻辑，结合Kripke语义与实数上的格群运算，通过带标签tableau系统获得coNEXPTIME上界，并建立模态-乘法片段的消割sequent演算及扩展阿贝尔逻辑的完备性。
2018-01-22 cs.LO
Modelling Multiplicative Linear Logic via Deep Inference
本文研究乘法线性逻辑中深推理系统与标准矢列演算之间的翻译关系，提出简化翻译并证明标准建模方法对翻译保持不变，同时给出一个文献中缺失的关于 par 与 tensor 数量的可证性必要条件。
2024-04-01 cs.LO math.LO
Multiplicative linear logic from a resolution-based tile system
我们提出了恒星的分辨率，一个“灵活的”瓦系统的基础上罗宾逊的一阶分辨率。在建立了恒星分辨率的正式定义和基本性质之后，我们展示了它的图灵完备性，并展示了它如何自然地表示计算与Horn子句和自动机以及DNA计算中使用的非确定性平铺结构。在第二部分和主要部分，通过使用恒星分辨率，我们正式和扩展的想法，一个新的替代证明网络理论概述了吉拉德在他的先验语法程序。特别是，我们编码的线性逻辑（MLL）的乘法片段的削减消除和逻辑正确性。最后，我们得到的完整性结果MLL和MLL扩展与所谓的MIX规则。通过扩展Girard的交互几何的思想，这表明了对逻辑和计算之间相互作用的新理解的第一步，其中线性逻辑被视为格式化计算的（构造）方式。
2022-07-18 cs.LO math.LO
Using Z3 to Verify Inferences in Fragments of Linear Logic
本文提出一种基于Z3定理证明器的Gentzen风格线性逻辑矢列式模板，用于自动验证推理规则，并在MLL+Mix和MILL两个片段上验证了若干导出推理规则。
2023-09-25 cs.LO
Normalization by Evaluation for the Lambek Calculus
Lambek的句法演算是直觉非交换线性逻辑乘法片段的演绎系统。作为资源的细粒度演算，它有许多应用，主要是在自然语言的形式化计算研究中。本文给出了逻辑连接词间具有乘法单位和合取的Lambek演算中导子的β-η-长范式演算。归约为范式遵循求值归一化（NbE）策略：（i）在Lambek演算的Kripke模型中求值导出;（ii）从所获得的语义值中提取范式。NbE算法的实现需要在正公式的Kripke解释中存在一个强单子，类似于具有虚假性和析取的直觉命题逻辑的扩展。NbE算法也可以通过对相关子结构逻辑的演算的微小变化来实例化，例如乘法和对偶直觉线性逻辑（MILL和DILL）。
2022-04-14 cs.LO
Normalization and sub-formula property for Lambek with product and PCMLL -- Partially Commutative Multiplicative Linear Logic
本文建立了直觉主义非交换逻辑的自然演绎或λ演算公式的规范化--它同时涉及交换和非交换连接词。这种演算首先介绍了德格罗特，而不是经典版本的Abrusci和Ruet承认充分熵，允许为了放宽到任何suborder。我们的结果还包括，作为一个特殊的情况下，正常化的自然演绎Lambek演算的产品，这是不足为奇的，但尚未证明。对于全熵的直觉非交换逻辑，至今没有一个证明网语法;对于语言应用，与自然演绎或多或少等价的逻辑演算由于缺乏标准的Curry-Howard同构而不方便。
2014-02-03 cs.FL cs.LO
Surface Proofs for Nonsymmetric Linear Logic (Extended Abstract)
证明了乘性线性逻辑中的一个证明可以表示为一个修饰曲面，使得两个证明仅当它们的曲面在几何上等价时，它们在逻辑上等价。这是arXiv的扩展摘要：1601.05372。
2017-01-18 cs.LO
From QBFs to MALL and back via focussing: fragments of multiplicative additive linear logic for each level of the polynomial hierarchy
在这项工作中，我们将探讨如何提取交替的时间界限从“集中”证明系统。我们的主要结果是获得片段的MALLw（MALL与削弱）完整的多项式层次的每一个级别。在一个方向上，我们编码QBF可满足性，并在另一个方向上，我们编码集中证明搜索，我们表明，这两个编码的组合保留量词交替，产生所需的结果。通过仔细地将众所周知的MALLw嵌入到MALL中，我们获得了MALL公式的类似描述，再次为多项式层次的每一级雕刻出完整的片段。这改进了MALLw和MALL都是PSPACE完备的著名结果。一个关键的见解是，我们必须改进聚焦的通常表示，以解释证明搜索中的确定性计算，这对应于不分支的可逆规则。这是为了我们可以更忠实地将集中证明搜索的阶段与它们的交替时间复杂度相关联。这个演示文稿似乎揭示了进一步的对偶性在水平上的证明搜索比通常的演示文稿，所以可能是进一步的证明理论的兴趣在其本身的权利。
2020-03-03 cs.LO
Linear Realisability over nets: multiplicatives (long version)
针对线性逻辑乘法片段，提出基于正交性的新可实现性模型，定义广义公理的截消，证明其对MLL*和MLL的适当性与完备性，解决广义公理下的可实现性建模问题。
2024-11-26 cs.LO
Resource-distribution via Boolean constraints
我们考虑的问题，搜索证明顺序表示逻辑与乘法（或内涵）连接词。具体来说，我们从线性逻辑的乘法片段开始，一方面扩展到线性逻辑及其添加剂，另一方面扩展到集束蕴涵逻辑BI的添加剂。我们给出了一个代数方法计算乘法规则中的侧公式的分布，一旦有足够的信息，它允许在证明的分支上确定公式的发生或不发生。这样一个规则的结论中的每个公式都被赋予一个布尔表达式。随着搜索的进行，生成一组布尔约束方程。我们表明，这样一组方程的解决方案确定了相应的证明给定的搜索。我们解释了一系列的战略，从懒惰的渴望，解决约束方程组。我们指出如何将我们的方法系统地应用到大家庭的相关系统。
2000-12-21 cs.LO
A Proof-theoretic Semantics for Intuitionistic Linear Logic
Department of Computer Science, University College London（伦敦大学学院计算机科学系）
本文扩展了Gheorghiu等人对直觉主义乘法线性逻辑的基扩展语义，为完整的直觉主义线性逻辑（包括模态连接词bang）提供了证明论语义，并讨论了处理bang连接词的挑战。
2026-06-12 cs.LO
A Categorical Semantics for Linear Logical Frameworks
本文提出了一种类型论，它把（直觉）线性类型与类型依赖相结合，从而适当地推广了直觉依赖类型论和完全线性逻辑。语法和完整的范畴语义的发展，后者在（严格）索引对称monoidal范畴的理解。以模块化方式处理各种可选类型的成形器。特别是，我们将看到，历史上备受争议的乘法量词和身份类型自然地产生于范畴考虑。这些新的乘法连接词的进一步特点是由几个身份有关的依赖类型论和线性逻辑通常的连接词。最后，详细研究了一类重要的模型，即由值在某个对称monoidal范畴内的族给出的模型。
2015-01-20 cs.LO
On the role of connectivity in Linear Logic proofs
Université Paris Cité（巴黎西岱大学）；Università Roma Tre（罗马第三大学）
本文研究了线性逻辑证明中连通性的作用，提出了一种几何条件将必要性质转化为充分条件，从而为线性逻辑的片段提供正确性标准。
2026-02-06 cs.LO
Introduction to linear logic and ludics, part II
本文是《线性逻辑和态极逻辑引论》一文的第二部分。它致力于证明网络，在有限的，但中心，框架的乘法线性逻辑和ludics，这是最近发展的目的是进一步揭示基本的互动性质的计算和逻辑。我们希望本文能对这一新的理论带来一些计算机科学方面的启示。
2005-01-19 cs.LO
Non-associative and projective linear logics
本文对乘法和加法联结词给出了Girard线性逻辑的一个非交换、非结合的弱化。额外的假设捕捉了定量测量的逻辑。
2022-01-06 cs.LO math.LO
Classical BI: Its Semantics and Proof Theory
我们提出了经典BI（CBI），一个新的除了家庭的聚束逻辑，起源于O 'Hearn和Pym的逻辑聚束蕴涵BI。CBI与现有的集束逻辑的不同之处在于，它的乘法连接词表现为经典的而不是直觉的（特别是经典否定的乘法版本）。在语义层面上，CBI公式具有正常的成束逻辑，读作关于资源的声明性语句，但其资源模型必然比其他成束逻辑具有更多的结构;原则上，它们满足每个资源都有唯一对偶的要求。在证明理论的层面上，一个非常自然的形式主义为CBI提供了一个显示演算à la Belnap，它可以被看作是一个概括的集束的BBI演算。在本文中，我们制定了上述模型理论和CBI的证明理论，并证明了一些基本结果的逻辑，最显着的完整性证明理论的语义。
2010-07-20 cs.LO
Phase Semantic Cut-elimination for Intuitionistic Linear Logic with Least and Greatest Fixed Points
Graduate School of Humanities and Human Sciences Hokkaido University（北海道大学人文科学研究院）；School of Computer Science University of Sheffield（谢菲尔德大学计算机学院）；Faculty of Humanities and Human Sciences Hokkaido University（北海道大学人文科学部）
研究具有最小和最大不动点的直觉主义命题乘加线性逻辑（$\mu$IMALL）的消去切割定理，通过定义相位语义，证明其可靠性与无切割完全性，改进前人论证方法来达成该定理的证明。
2026-07-23 cs.LO
String Diagrams for Regular Logic (Extended Abstract)
正则逻辑可以被看作是正则范畴的内部语言，但逻辑本身一般不被给予范畴化的处理。本文用集合T上的自由正则范畴FRG（T）来理解正则逻辑的语法和证明规则。从这个观点来看，正则理论是从一个合适的2-范畴的上下文--FRG（T）中的2-范畴的关系--到偏序集的2-范畴的某些monoidal 2-函子。这样的函子给每个上下文中的公式集赋值，并按蕴涵排序。我们把这样一个2-函子称为一个正则演算，因为它自然地产生了一个图形化的弦图演算的精神Joyal和街。我们将证明，每一个自然范畴都有一个相关联的正则演算，反过来，从每一个正则演算，我们可以构造一个正则范畴。
2020-09-15 cs.LO
Exponentially Handsome Proof Nets and Their Normalization
Retoré引入了Handsome Proof Nets作为乘法线性逻辑的语法。这些证明网是通过配备了满足简单拓扑条件的顶点划分的上图（表示公式的图）来定义的。在本文中，我们将这种语法扩展到乘法线性逻辑单位和指数。为此，我们开发了一个新的健全和完整的证明系统的逻辑，强制执行一个更强的概念，证明等价的一个通常认为在文献中。然后，我们定义组合证明，一个图形证明系统，能够捕捉语法的证明等价性，为切自由片段的演算。最后，我们通过定义指数英俊的证明网组合证明削减和定义这种语法的内部规范化程序的文件。
2021-12-30 cs.LO
A categorical reduction system for linear logic
图追逐不是一件容易的任务。如果我们有一个机械的方法来判断给定的两个态射是否彼此相等，则相干性在广义上成立。一个简单的方法是将一个相关的范畴转化为一个演算，其中图追踪的指令以重写规则的形式给出。我们将这一思想应用于线性逻辑的范畴语义。我们直接在语义的自由范畴上建立了一个演算。它使我们能够执行图表追踪，本质上是由重写规则领导的单向计算。我们验证了这种演算的弱终止性质。这为图表追踪的机械化迈出了第一步。
2020-10-08 cs.LO
Extending Action Logic with Omega Iteration
本文通过引入欧米伽迭代扩展动作逻辑，提出了一个证明系统并证明了其割可接受性及可证明性谓词的复杂性界限。
2025-12-07 cs.LO math.LO
A Diagrammatic Algebra for Program Logics
本文通过引入带 $\oplus$ 上迹的带图和 Kleene-Cartesian 双范畴，为命令式程序提供了一种图解记法与证明系统，其表达能力至少与 Hoare 逻辑相当。
2024-10-04 cs.LO
A Linear-logical Reconstruction of Intuitionistic Modal Logic S4
本文提出了一种“模态线性逻辑”，它将直觉模态逻辑S4（IS 4）用线性逻辑来表示，建立了从IS 4到它的Girard翻译的S4-版本。它对模态逻辑的扩展是非-这是微不足道的，因为S4模态和指数模态的简单组合导致两种模态之间的不期望的相互作用。为了解决这个问题，我们引入了一个扩展的直觉乘法指数线性逻辑与模态相结合的S4模态和指数模态，并表明它承认从IS 4的声音翻译。通过Curry-Howard对应，我们进一步得到了Pfenning和Davies为分阶段计算所提出的模态微积分的交互几何机器语义。
2019-04-24 cs.LO
Modality for Free: Notes on Adding the Tarskian Möglichkeit to Substructural Logics
我们简要地研究了模态公式，可以得出乘法加法线性逻辑（MALL）和一些扩展，通过使用Tarksi的扩展模态算子。我们还将它与模态逻辑K的一个子结构形式作了简单的比较。
2011-05-08 cs.LO math.LO
Least and Greatest Fixed Points in Linear Logic
MALL（乘法，加法线性逻辑）的一阶理论仅在等式上是一个有趣但弱的逻辑，因为它不能捕获无界（无限）行为。而不是通过增加指数（！和？），我们添加最小和最大不动点算子。由此产生的逻辑，我们称之为muMALL，满足两个基本的证明理论性质：我们建立弱规范化，我们设计了一个集中的证明系统，我们证明完整的。第二个结果提供了一个强范式的无切割证明结构，可用于，例如，帮助自动化证明搜索。我们展示了如何将这些基础应用于直觉逻辑。
2010-11-30 cs.LO
Syllogisms in Rudimentary Linear Logic, Diagrammatically
我们提出了一个阅读的传统三段论在一个片段的命题直觉乘法线性逻辑，并证明，相对于一个图解逻辑演算，我们介绍了在以前的文件，一个三段论是可证明的，在这样一个片段，当且仅当它是图解可证明的。我们把这个结果推广到带有补充项的德摩根三段论，这是关于传统情况下图解推理系统的适当扩展，以及在前面提到的线性逻辑片断中对这种德摩根式三段论的相应解读。
2013-02-28 cs.LO math.LO
Taylor expansion in linear logic is invertible
本文证明MELL证明网的泰勒展开是单射的，即不同证明网对应不同展开，进而推出关系模型对MELL证明网的完备性，即相等性恰由消割公理化。
2018-12-06 cs.LO
Bifurcation Logic: Separation Through Ordering
CNRS（法国国家科学研究中心）；LORIA（洛林研究与信息系统实验室）；University College London（伦敦大学学院）；Institute of Philosophy（哲学研究所）；University of London（伦敦大学）
分支逻辑通过有序分离结合模态算子和分离 conjunction，用于多代理访问控制，提供了一种可判定的逻辑框架。
2025-11-26 cs.LO
Modelling Linear Logic Without Units (Preliminary Results)
我们描述了（乘法）线性逻辑的无单位片段的范畴模型的概念。基本定义使用promonoidal范畴，我们也给出了一个等价的初等公理化。
2005-04-03 cs.LO math.CT math.LO
MALL proof equivalence is Logspace-complete, via binary decision diagrams
逻辑中的证明等价问题是判定两个证明是否模一组规则置换等价的问题，这些规则置换反映了其割消过程的交换转换。因此，它与证明网的问题有关：找到具有良好计算特性的等价证明类的规范代表。它也可以看作是自由范畴概念对应于逻辑的语词问题。最近已经表明，MLL（线性逻辑的单位片段的乘法）中的证明等价是PSPACE-完全的，这排除了这种特定逻辑的证明网的任何低复杂度概念。由于它是另一个片段的线性逻辑，试图定义一个完全令人满意的低复杂度的概念证明网还没有成功，到目前为止，我们研究证明等价MALL-（乘法加法没有单位片段的线性逻辑），并发现一种情况是完全不同的MLL的情况。事实上，我们证明在MALL等价对应（根据AC 0减少）等价的二元决策图，一个数据结构广泛用于表示和分析布尔函数有效。我们证明了这两个等价问题是LOGSPACE完备的。如果这在技术上为MALL-的证明网问题的完整解决方案留下了可能性，那么与二元决策图建立的关系实际上表明了这个问题的否定解决方案。
2015-04-17 cs.LO
Fuzzy Aristotelian Diagrams
本文以基于二值逻辑的亚里士多德图为起点，引入了模糊亚里士多德图并给出其数学表述，同时概述了容纳该对象的数学宇宙的特征。
2025-07-14 cs.LO
The exponential logic of sequentialization
本文通过将跳跃机制内化到乘法线性逻辑（MLL）的扩展中，引入跳跃公式约束图的序列化过程，揭示了序列化的指数逻辑。
2023-11-17 cs.LO
Focused Proof-search in the Logic of Bunched Implications
集束蕴涵（BI）逻辑自由地组合了加法和乘法连接词，包括蕴涵;然而，尽管其证明理论得到了充分的研究，但BI中的证明搜索一直是一个难题。聚焦原则是对证明-搜索空间的一种限制，它可以捕获各种目标导向的证明-搜索过程。在本文中，我们表明，集中的证明搜索是完整的BI首先重新制定传统的束的嵌套序列，使用更简单的数据结构，然后与极化和集中的变体，我们显示是健全的和完整的，通过削减消除参数。这建立了一个操作语义集中证明搜索的逻辑集束的影响。
2021-01-26 cs.LO
A first-order logic for string diagrams
用弦图进行方程推理提供了一种直观的方法来证明对称幺半范畴中态射之间的方程。这可以扩展到使用一个简单的图形语法来证明无限族的方程，称为！-方框符号虽然这确实大大增加了字符串图的证明能力，但以前超越等式推理的尝试在很大程度上是临时的，因为缺乏合适的逻辑框架来进行涉及！箱.在本文中，我们将等式推理扩展为！框到一个完全成熟的一阶逻辑，称为连接，含义和全称量化！-箱.这个逻辑，叫做！L，则足够丰富以适当地形式化归纳原理，箱.然后我们建立一个标准模型！并给出一个非交换双代数的定理的例子证明！L，这是无法通过等式推理单独获得的。
2015-05-02 cs.LO math.CT
On Quantifiers for Quantitative Reasoning
University of Strathclyde（斯特拉斯克莱德大学）
本文提出了一种基于实数的量化谓词逻辑，引入非线性、线性加法和线性乘法连接词，并探讨了均值和调和均值作为量词的语义，同时展示了softmax和Rényi熵在该逻辑中的应用。
2025-12-02 cs.LO math.LO
Probabilistic Linear Logic Programming with an Application to Bayesian Network Computations (Extended Version)
University of Southern Denmark（南丹麦大学）；Roma TRE University（罗马三大学）
本文提出probLO，一种将贝叶斯网络整合到线性逻辑编程中的方法，通过多头Prolog-like方法和切片操作实现概率计算。
2026-02-24 cs.LO
A MALL Geometry of Interaction Based on Indexed Linear Logic
本文为乘法-加法线性逻辑构建基于索引线性逻辑的交互几何，扩展了Haghverdi-Scott范畴框架，利用索引处理加法消割的叠加、擦除和收缩，并证明执行公式沿消割不变，收敛到无割证明的指称。
2020-07-28 cs.LO
Extended Lambek calculi and first-order linear logic
CNRS（法国国家科学研究中心）；LaBRI（波尔多计算机科学实验室）
一阶乘法直觉线性逻辑（MILL 1）可以看作是Lambek演算的一个扩展。除了MILL 1的片段对应于Lambek演算（Moot & Piazza 2001），我将展示MILL 1的片段，它们生成多种上下文无关语言，并对应于Morrilll等人的位移演算。
2013-05-27 cs.CL cs.LO
From Linear Logic to Cyclic Sharing
我们提出了一个翻译从乘法指数线性逻辑到一个简单类型的λ演算与循环共享。这个翻译是从对追踪monoidal范畴的int-结构的简单观察中得出的。事实证明，翻译是一个混合的按名称呼叫CPS翻译和几何互动为基础的解释。
2019-04-15 cs.LO cs.PL
On Geometry of Interaction for Polarized Linear Logic
我们提出了乘法极化线性逻辑（MLLP）的交互几何（GoI）模型，MLLP是Olivier Laurent的极化线性逻辑的乘法片段。这是通过将多个点均匀地添加到GoI的各种分类模型来完成的。在极化证明理论中，多点在语义上表征证明网络的动态性方面发挥着重要作用。例如，它们允许我们描述极化的关键特征，聚焦，以及我们构建具体极化GoI模型的基础。我们的方法两极分化GoI涉及两个独立的研究，根据不同的分类角度的GoI。(i)受Abramsky，Haghverdi和Scott工作的启发，定义了一个极化的GoI情况，其中多点被添加到配备有自反对象$U$的跟踪monoidal类别。使用这个框架，吉拉德的执行公式的分类版本的定义，以及GOI解释MLLP，证明。运行的执行公式示出的特征的聚焦属性（从而极性），以及动态的削减消除。(ii)Joyal-Street-Verity的Int构造是GoI建模的另一个基本范畴结构。在这里，我们调查它在一个多点设置。我们的演示文稿产生了一个紧凑的版本Hamano-Scott的极化类别，从而指称模型MLLP。这些产生于正和负对象的monoidal范畴之间的逆变对偶性，以及它们之间的适当双模结构（代表“非聚焦证明”）。最后，作为上述（ii）的一个特殊情况下，MLLP的紧凑模型也提出了基于Rel（集合和关系的范畴）配备了多点。
2017-04-07 cs.LO
Formalizing Timing Diagram Requirements in Discrete Duration Calulus
已经提出了几种时序逻辑来正式化硬件和嵌入式控制器的时序图要求。这些包括LTL、离散时间MTL和最近的行业标准PSL。然而，时序图的简洁性和视觉结构并没有被他们的公式充分捕捉。区间时序逻辑QDDC是一种高度简洁和可视化的表示法，用于指定行为模式。在本文中，我们提出了一个实际有用的符号称为SeCeCntnl，增强了否定自由片段的QDDC与功能的名词和有限的活性。我们表明，时序图可以自然（成分）和successly正式在SeCeCntnl相比，PSL和MTL。我们给出了一个线性时间翻译时序图SeCeCntnl。作为我们的第二个主要结果，我们提出了SeCeCntnl到QDDC的线性时间翻译。这使得QDDC工具，如DCVALID和DCSynth，可用于检查时序图要求的一致性，以及自动合成属性监视器和控制器。我们给出了一个矿泵控制器和总线仲裁器的例子来说明我们的工具。给出了理论分析，我们表明，所提出的SeCeCntnl，可满足性和模型检验具有初等复杂性相比，非初等复杂性的全逻辑QDDC。
2017-05-12 cs.LO
