Exponentially Handsome Proof Nets and Their Normalization
Retoré引入了Handsome Proof Nets作为乘法线性逻辑的语法。这些证明网是通过配备了满足简单拓扑条件的顶点划分的上图（表示公式的图）来定义的。在本文中，我们将这种语法扩展到乘法线性逻辑单位和指数。为此，我们开发了一个新的健全和完整的证明系统的逻辑，强制执行一个更强的概念，证明等价的一个通常认为在文献中。然后，我们定义组合证明，一个图形证明系统，能够捕捉语法的证明等价性，为切自由片段的演算。最后，我们通过定义指数英俊的证明网组合证明削减和定义这种语法的内部规范化程序的文件。
2021-12-30 cs.LO
Bipolar Proof Nets for MALL
在这项工作中，我们提出了一个计算范式的基础上，并行和增量建设的证明网（de-sequentialized或图形证明）的纯乘法和加法片段的线性逻辑，资源意识的经典逻辑的细化。此外，我们设置了一个correspondence- dence之间的这种范式和那些更务实的启发事务或分布式系统。特别是，我们可以解释为一个模型的超级ACID（或合作）的分布式事务系统（典型的，多数据库）的交易的建设添加剂证明网。
2012-10-22 cs.LO
Complexity of correctness for pomset logic proof nets
我们表明，它是coNP-完全的，以决定是否一个给定的证明结构的pomset逻辑是一个正确的证明网，使用图论在我们以前的文件（arXiv：1901.10247）。
2023-01-23 cs.LO
From Proof Nets to the Free *-Autonomous Category
本文的第一部分给出了全乘法线性逻辑的证明网理论，包括两个单元。它自然地扩展了著名的无单位乘法证明网理论。链接不再是公理链接的集合，而是一棵树，其中公理链接是子树。这些树将根据基于图重写的简单形式的等价关系来识别。我们展示了切割消除的序列化和强规范化的标准结果。在本文的第二部分中，我们证明了强制执行的证明是这样的两个结论的证明网类定义的自由 *-自治范畴。
2006-10-05 cs.LO
Perpetual Free-choice Petri nets are lucent -- proof of a theorem of van der Aalst using CP-exhaustions
本文通过CP-子网穷举法证明van der Aalst定理，即永久自由选择Petri网是清晰的，并用初等方法分析所得T-系统。
2021-11-10 cs.LO
Bayesian Networks and Proof-Nets: the proof-theory of Bayesian Inference
IRIF, Université Paris Cité - CNRS（IRIF，巴黎西岱大学-法国国家科学研究中心）
本文提出通过证明论方法将贝叶斯推断与线性逻辑中的证明图形相结合，探讨其组合性和计算效率。
2026-02-03 cs.LO
On paths-based criteria for polynomial time complexity in proof-nets
Girard的轻型线性逻辑（LLL）在证明为程序的范例中以多项式时间为特征，并在切割消除上有界。这种逻辑依赖于分层原则和“一门”原则，这些原则后来分别在系统L^4和L^3a中得到推广。每个系统都有自己复杂的Ptime可靠性证明。在本文中，我们提出了一个广泛的充分标准Ptime健全的线性逻辑子系统，基于研究的路径内的证明网，因式分解证明现有系统的健全性，并可能用于未来的系统。作为一个额外的收获，我们的界限代表任何减少战略，而在文献中的大多数界限只代表一个特定的战略。
2014-05-19 cs.LO
Light Affine Logic (Proof Nets, Programming Notation, P-Time Correctness and Completeness)
本文是一个结构介绍轻仿射逻辑，其直观的片段。轻仿射逻辑有一个多项式成本削减消除（P时间正确性），并编码所有P时间图灵机（P时间完整性）。通过引入直觉轻仿射逻辑的证明网，证明了P-时间正确性。P-Time的完整性通过一个非常紧凑的程序符号得到了充分的证明。一方面，P-Time正确性的证明描述了切割消除的复杂性是如何控制的，这要归功于利用证明网的结构属性的适当切割消除策略。这使得我们能够很好地理解“段落”模态的含义，这是轻逻辑的一个特点。另一方面，P-时间完备性的证明，以及大量的编程实例，给出了一个非平凡的任务，编程资源的限制，使用直觉轻仿射逻辑推导程序的味道。
2000-06-05 cs.LO
An introduction to Differential Linear Logic: proof-nets, models and antiderivatives
微分线性逻辑丰富了线性逻辑与额外的逻辑规则的指数连接，对偶的通常规则的遗弃，削弱和收缩。本文提出了微分线性逻辑的证明网语法及其指称模型的范畴公理化。我们还介绍了一个简单的分类条件下，这些模型的一般反导数操作变得可用。最后，我们简要地描述了集合和关系的模型，并给出了有限性空间和线性和连续函数的模型更详细的说明。
2016-06-06 cs.LO
An application of parallel cut elimination in multiplicative linear logic to the Taylor expansion of proof nets
本文研究MLL证明网并行消去的组合性质，通过路径约束保证无限加权和归约的有限性，并证明该约束适用于MELL泰勒展开中的微分网，为线性逻辑定量语义提供充分条件。
2021-12-17 cs.LO
An Explicit Framework for Interaction Nets
交互网络是一种图形形式主义，灵感来自线性逻辑证明网络，通常用于研究高阶重写，例如\Beta -归约。交互网络的传统表示是基于图论的，并依赖于图论的基本性质。我们在这里给一个更明确的介绍的基础上，从吉拉德的几何相互作用的概念：相互作用网的部分排列和组成的网络，胶合，是来自执行公式。然后，我们定义上下文和约简为规则的上下文闭包。我们证明了我们的框架内的减少强融合，并显示如何互动网可以被视为商的一些广义的证明网。
2010-12-13 cs.LO
Proof nets and the call-by-value lambda-calculus
本文详细介绍了按值调用λ演算（的一种变体）与线性逻辑证明网之间的关系。为了实现两个系统之间的强互模拟，我们对演示进行了仔细的调整：微积分上的每一个重写步骤都映射到网络上的单步的，反之亦然。通过这种方式，我们得到了证明网的代数重构。此外，我们为我们的证明网提供了一个简单的正确性标准，它以一种不寻常的方式使用盒子。
2013-03-29 cs.LO cs.PL
Unification nets: canonical proof net quantifiers
MLL（unit-free Multiplicative Linear Logic，无单位乘法线性逻辑）的证明网是证明的简洁图形表示，在某种意义上，它们是规范的，因为它们抽象掉了语法冗余，例如非交互规则的顺序。我们认为，吉拉德的扩展MLL 1（一阶MLL）未能规范，因为冗余存在的证人，并提出规范MLL 1证明网称为统一网没有他们。例如，虽然有无限多个无割Girard网$\forall x Px \vdash \exists xPx$，每个任意选择一个证明$\exists x$，但有一个唯一的无割统一网，没有指定的证明。冗余的存在性见证导致Girard的MLL 1网遭受严重的复杂性问题：（1）割消是非局部的和指数时间（和空间）的，（2）一些序列需要指数大的无割Girard网。统一网解决了两个问题：（1）割消是局部的和线性时间的，以及（2）无割统一网随着网络的大小线性增长。由于某些统一网比相应的Girard网和后续证明呈指数级小于，因此需要技术上的微妙性来确保正确性是多项式时间（二次）的。这些结果通过更广泛的方法论见解扩展到MLL 1之外：对于规范量词，标准的并行/顺序二分法的证明网失败了;还需要一个隐式/显式的见证二分法。正在进行的工作将统一网络扩展到添加剂，并使用它们将组合证明[无语法证明，数学年鉴，2006]扩展到经典一阶逻辑。
2018-02-09 cs.LO math.LO
Canonical Proof nets for Classical Logic
证明网为模规则排列的证明提供了抽象的对应物;其思想是，如果两个证明具有相同的底层证明网，则它们本质上是相同的证明。因此，提供一个令人信服的证明网络对应于经典的微积分证明是理解经典微积分证明的重要一步。通过令人信服，我们的意思是：（a）应该有一个典范函数从证明网络的证明，（b）应该有可能检查网络的正确性在多项式时间，（c）每个正确的网络应该是可获得的从一个微积分证明，（d）应该有一个削减消除程序，保持正确性。以前的尝试给证明网类对象的命题经典逻辑已经失败了至少一个上述条件。在[23]中，作者给出了满足（a）和（b）的证明网（扩展网）的演算;文章定义了与扩展网对应的证明演算，但没有给出（c）的显式证明。该演算称为LK \ast，是一种新的具有加法和乘法析取规则的单边演算.本文（[23]的一个自包含的扩展版本）给出了关于LK \ast的扩展网的（c）的一个充分证明，并且另外给出了扩展网内部的一个割消元过程--这使得扩展网成为满足所有四个准则的经典逻辑的第一个证明网概念。
2012-03-19 cs.LO math.LO
Proof Diagrams for Multiplicative Linear Logic
证明网的原始思想可以通过交互网语法来表达。为了保证证明结构和正确证明之间的对应性，需要额外的机制，如切换、跳转和图连通性。在本文中，我们给出了一个解释的证明网的语法字符串图。即使我们失去了标准的证明等价性，我们的结构允许定义一个框架，在这个框架中，可以在线性时间内验证图的合理性和良好类型。
2017-01-18 cs.LO
Multiparty Sessions based on Proof Nets
我们解释线性逻辑证明网的术语语言的基础上Solos演算。该系统包括一个同步机制，通过逻辑的保守扩展获得，能够定义非确定性行为和多方会话。
2014-06-13 cs.LO cs.PL
Proof Nets, Coends and the Yoneda Isomorphism
证明网提供置换无关的证明表示，并用于研究monoidal范畴的一致性问题。研究了二阶乘法线性逻辑（MLL2）的一个一致性问题，即用端和余端刻画量词解释所生成的证明的等价性问题.我们提供了一个紧凑的表示证明网MLL2相关的米田同构的片段。通过调整“重新布线的方法”中使用的一致性结果的明星自治类别，我们定义了一个等价关系的证明网称为“重新见证”。我们证明，这种关系的特点，在这个片段中，产生的等价coends。
2019-04-15 cs.LO math.LO
Sublogarithmic uniform Boolean proof nets
使用证明即程序的对应关系，Terui能够比较两种并行计算模型：布尔电路和乘法线性逻辑的证明网。莫格比尔等al.给出了一个对数空间转换，使我们能够比较它们作为统一复杂性类的计算能力。本文提出了一种新的翻译AC0和集中在一个更简单的限制概念的一致布尔证明网。然后，我们可以对恒定深度的电路进行编码，并比较对数空间下的复杂度类，这是以前的翻译无法达到的。
2012-01-05 cs.CC cs.LO
Proof nets for the Displacement calculus
CNRS（法国国家科学研究中心）
我们提出了一个证明网演算的位移演算，并证明其正确性。这是第一个直接对位移演算进行建模的证明网演算，而不是通过某种形式转换成另一种形式。证明网演算为使用置换演算进行解析和证明搜索开辟了新的可能性。
2016-06-06 cs.CL cs.LO
Proof nets for Herbrand's Theorem
本文探讨了经典逻辑证明论的两个中心结果：根森的微积分割消与赫布兰德的“基本定理”之间的联系。本文从Herbrand定理的一种高度结构化的表达方式Miller的扩展树证明出发，定义了一阶经典逻辑的无弱化证明网演算，并给出了一个弱规范化割消过程。在这种演算中，不可能对割消的汇合给出通常的反例，但它仍然是不汇合的，这使人们相信经典逻辑本质上是不汇合的。
2010-05-21 cs.LO math.LO
Generalised Proof-Nets for Compact Categories with Biproducts
正如传统的函数程序可以被理解为直觉主义逻辑中的证明一样，量子过程也可以被视为合适逻辑中的证明。我们描述这样一个逻辑，紧凑的闭范畴和biproducts的逻辑，提出了作为一个微积分和作为一个系统的证明网。这种逻辑捕捉了在经典控制下表示量子过程所需的大部分必要结构，同时对细节保持不可知论。我们演示了如何表示量子过程的证明网，并表明量子过程的动态行为被捕获的逻辑的削减消除过程。我们表明，削减消除程序是强烈规范化：也就是说，每一个法律的简化证明网络的方式导致相同的，唯一的，正常的形式。最后，采取一些初始的操作作为非逻辑公理，我们表明，由此产生的类别的证明网是一个表示的自由紧凑的闭范畴与这些操作所产生的双产品。
2009-03-30 cs.LO math.CT
Taylor expansion in linear logic is invertible
本文证明MELL证明网的泰勒展开是单射的，即不同证明网对应不同展开，进而推出关系模型对MELL证明网的完备性，即相等性恰由消割公理化。
2018-12-06 cs.LO
A new graphical calculus of proofs
我们提供了一个简单的图形表示的直觉逻辑的证明，这是灵感来自证明网和交互网（两个形式主义起源于线性逻辑）。这种证明的图形演算继承了每一种方法的良好特性，但不受它们的约束。通过Curry-Howard同构，该表示同样适用于λ演算，提供了函数计算的另一种图形表示。
2011-02-14 cs.LO
Unique perfect matchings, forbidden transitions and proof nets for linear logic with Mix
本文证明MLL+Mix证明网正确性等价于完美匹配唯一性，并据此提出线性时间判据、拟线性顺序化算法及次多项式复杂性刻画，同时将依赖关系与王国排序关联到花朵概念。
2020-02-27 cs.LO
The relational model is injective for Multiplicative Exponential Linear Logic
本文证明了乘性指数线性逻辑（MELL）的一个完备性结果：证明了关系模型对于MELL证明网是单射的，即关系模型中MELL证明网之间的相等性是用割消法精确公理化的。
2016-05-10 cs.LO
Multiplicative-Additive Focusing for Parsing as Deduction
虚假歧义是指语法中不同的派生词可能分配相同的结构阅读，导致句法分析搜索空间冗余和句法分析效率低下的现象。理解这个问题取决于识别推导的基本数学结构。这在上下文无关文法的情况下是微不足道的，其中解析结构是有序树;在范畴文法的情况下，解析结构是证明网。然而，关于乘法内在的证明网尚未给出位移演算，和证明网添加剂，其中有应用多态性，涉及。在这里，我们接近乘加伪歧义的证明理论的聚焦技术的手段。
2015-11-13 cs.LO
Neural Proof Nets
Utrecht Institute of Linguistics OTS, Utrecht University（乌得勒支大学乌得勒支语言学研究所OTS）；LIRMM, Université de Montpellier, CNRS（法国国家科学研究中心蒙彼利埃大学计算机信息与机器人微电子实验室）
线性逻辑和线性λ演算在自然语言形式和意义的研究中有着悠久的传统。在线性逻辑的证明演算中，证明网特别令人感兴趣，它提供了一种有吸引力的推导几何表示，不受传统证明理论格式的官僚复杂性的影响。基于集合论学习的最新进展，我们提出了一种基于Sinkhorn网络的证明网络的神经变体，这使我们能够将解析转换为提取句法原语并将其排列成对齐的问题。我们的方法诱导了一个批处理效率，端到端的差异化架构，实现了一个正式接地，但高效的神经符号解析器。我们测试了我们的方法，一个数据集的类型逻辑推导的书面荷兰语，在那里它设法正确地将原始文本句子转换成证明和线性λ演算的条款，准确率高达70%。
2020-09-26 cs.CL cs.LG cs.LO
Geometry of Interaction for MALL via Hughes-vanGlabbeek Proof-Nets
本文首次提出了一种基于Hughes-vanGlabbeek（HvG）的乘加线性逻辑（MALL）证明网的交互作用几何（GoI）解释。我们的GoI动态捕捉HvG的几何正确性标准-切换循环条件-代数算子。我们的新成分是一个标量扩展的 *-代数Girard的 *-环的部分等距的布尔多项式环的文字的特征权为不定。为了捕捉反馈所产生的削减，我们构造了一个更细粒度的执行公式。这个执行公式的扩展比乘法GoI的切片集合更长，因此更难证明终止。我们的GoI给出了一个动态的，语义的布尔值（特别是，修剪子证明），转换的权重（特别是，阿尔法转换），和添加剂（共）收缩，特有的添加剂证明理论。我们的执行公式的终止被示出为对应于HvG的切换标准。我们的执行公式的切片限制（通过折叠布尔结构）产生了众所周知的对应关系，显式或隐式在以前的作品乘法GoI，执行公式的收敛性和证明网的非循环性之间。反馈所产生的执行公式，通过限制到布尔多项式结构产生自主定义的特征权重之间的削减从其余的特征权重。
2018-07-08 cs.LO math.LO
A Coding Theoretic Study on MLL proof nets
编码理论对现实世界的应用非常有用。一个明显的例子是数字电视。基本上，编码理论是研究一种检测和/或纠正可能是真或假的数据的方法。此外，编码理论是数学的一个领域，其中数学的许多分支之间存在相互作用，例如，抽象代数、组合数学、离散几何、信息论等。本文提出了一种利用编码理论分析乘法线性逻辑证明网的新方法。我们定义家庭的证明结构，并为每个家庭引入一个度量空间。在每个家庭中，1。MLL证明网是真码元; 2.不是MLL证明网的证明结构是错误的（或损坏的）代码元素。我们的度量的定义优雅地反映了乘法连接词的对偶性。在本文中，我们表明，在框架中的一个错误检测是可能的，但一个错误纠正没有。我们的证明的不可能性的一个纠错是有趣的，在这个意义上说，证明理论的财产证明使用图论的论点。此外，我们表明，仿射逻辑和MLL + MIX是不适合这个框架。这就解释了为什么MLL比类似的逻辑更好。
2010-07-06 cs.DM cs.LO
Proof nets and the instantiation overflow property
实例化溢出是那些二阶类型的属性，对于这些二阶类型，完全理解的所有实例都可以从原子理解的实例中推导出来。换句话说，当可以通过原子多态性键入实现应用于该类型的完整提取规则的实例的“扩展项”时，该类型具有实例化溢出。这一性质是在由著名的罗素-普拉维茨翻译逻辑连接词到系统F中所产生的类型的情况下进行研究的，但并不局限于这样的类型。此外，它可以与函子多态性有关，函子多态性是系统F中参数性的一种众所周知的范畴方法。在本文中，我们研究的实例溢出性质，利用表示的派生通过线性逻辑证明网。我们开发了一个几何的方法，实例化溢出产生更深入的理解的结构的扩展条款和拉塞尔-Prawitz类型。我们的主要结果是一类类型的形式$\forall XA$，其中$A$是一个简单的类型，它享有实例化溢出属性，通过推广的Russell-Prawitz类型的特征。
2018-03-25 cs.LO math.LO
Taming Modal Impredicativity: Superlazy Reduction
纯的或无类型的线性逻辑证明网是图灵完备的，一旦割消被认为是计算。我们引入模态不可预测性作为不可预测性的一种新形式，从复杂性的角度来看，导致割消的复杂性是有问题的。模态不可预测性发生在当在约简期间，盒子b的残差的结论与属于b的另一个残差内的证明网的节点相互作用时。从技术上讲，超级惰性归约是一种新的归约概念，允许控制模态不可预测性。更具体地说，superlazy reduction仅在所有副本都打开时才复制一个盒子。这使得减少证据网的总成本是有限的和可预测的。具体来说，应用于任何纯证明网的超惰性归约都需要原始递归时间。此外，任何原始递归函数都可以通过超惰性归约由纯证明网计算。
2008-10-17 cs.LO
Proof identity for mere mortals
证明恒等式问题：什么时候两个证明是相同的？当人们反思数学实践时，这个问题自然会出现。这个问题可以理解为对数理逻辑的挑战，事实上，在证明论文献中可以找到关于这个问题的各种观点。从证明理论的角度来看，挑战是通过制定新的演算，消除“官僚主义”;技术，如规范化和削减消除，以及证明压缩，被采用。在这份说明中，一个新的角度对证明身份的问题进行了概述。新的方法采用的概念和自动定理证明的工具，并补充了来自纯证明理论的理论观点。实际的方法说明了来自TPTP问题库的实验。
2014-03-04 cs.LO
Proof Identity and Categorical Models of BV
University of Southern Denmark（南丹麦大学）；University of Sussex（萨塞克斯大学）；Inria and LIX, Ecole Polytechnique, Institut Polytechnique Paris（法国国家信息与自动化研究所与巴黎综合理工学院LIX实验室，巴黎理工学院）；Université Paris-Saclay, CNRS, ENS Paris-Saclay, Inria, Laboratoire Méthodes Formelles（巴黎萨克雷大学、法国国家科学研究中心、巴黎萨克雷高等师范学院、法国国家信息与自动化研究所、形式方法实验室）
本文提出BV证明身份的概念，基于原子流定义，以增强BV范畴并证明其对逻辑的正确性。
2026-04-28 cs.LO
Sequentialization for full N-Graphs via sub-N-Graphs
自从Girard（1987）提出了MLL-的证明网以来，出现了一些关于其可靠性证明的研究。Bellin & Van de Wiele（1995）提出了一个基于帝国和王国性质的优雅证明，Robinson（2003）提出了一个简单的推广，用于经典逻辑的证明网。在2014年，这些研究的一个扩展被提出来，通过子N-图的概念来获得具有合取、析取和否定连接词的N-图片段的序列化定理的证明。N-Graphs是一个具有多个结论的对称自然演绎演算，它采用Danos-Regnier准则，具有散焦可切换的链接。在本文中，我们提出了一个完整的命题经典N-图的序列化，显示如何找到一个分裂节点的证明，即使在中间的放电假设的整体规则。
2018-03-01 cs.LO
The Abstract Machinery of Interaction (Long Version)
本文回顾了Mackie和Danos & Regnier提出的基于Girard交互几何的交互抽象机（Interaction Abstract Machine，IAM）。它是一个不寻常的机器，不依赖于环境，在线性逻辑证明网络上呈现，其可靠性证明是复杂的，并通过各种其他形式主义。在这里，我们提供了一个新的直接证明其正确性的基础上，金沙的改进，一个自然的概念互模拟的变体。此外，我们的证明进行了一个新的介绍IAM，定义为一台机器直接作用于$λ$ -条款，而不是线性逻辑证明网。
2020-07-09 cs.LO cs.PL
A New Conjecture About Identity of Proofs
证明论的一个中心问题是寻找证明的同一性的标准，也就是说，当两个不同的形式推导可以被认为是表示同一个逻辑论证时。在文献中，人们发现标准是基于证明规范化（两个派生表示相同的证明时，他们有相同的标准形式）或正式派生与图论结构的关联（两个派生表示他们相同的证明时，他们与相同的图）。在本文中，我们认为一个新的标准，从解释的形式规则和推导作为自然变换的一个合适的种类的证明身份。我们表明，从这种解释所产生的自然性条件捕捉在一个统一的和优雅的方式中的几种形式的“规则排列”，发现在证明系统的命题，一阶和二阶逻辑。
2021-10-06 cs.LO math.LO
Elimination and cut-elimination in multiplicative linear logic
我们将乘法线性逻辑中的每个证明结构与一个理想相关联，该理想将证明的逻辑内容表示为多项式方程。我们展示了如何削减消除乘法证明网对应的Buchberger算法的实例计算Gröbner基地消除理论。
2022-07-22 cs.LO math.LO
