On extracting variable Herbrand disjunctions
通过证明挖掘获得的一些定量结果采取可能取决于附加参数的Herbrand析取的形式。我们试图阐明这一事实，通过扩展到一阶算术的证明Herbrand的定理，由于Gerhardy和Kohlenbach使用的功能解释。
2022-02-24 math.LO
Herbrand's Fundamental Theorem: The Historical Facts and their Streamlining
利用Heijenoort未发表的广义量化规则，讨论了Herbrand基本定理的证明，给出了Heijenoort对Herbrand“假引理”的修正，并给出了一个教学实例.虽然我们主要关注的是赫布兰德基本定理的内部结构及其性质和深度问题，但我们也讨论了它的历史背景的外部问题，以及伯奈斯为什么称它为“谓词逻辑的中心定理”，并认为它的表达形式是“简洁而恰当的”。
2014-08-14 cs.LO math.LO
Herbrand's Theorem in Refutation Schemata
针对含归纳证明的消去切问题，本文提出模式替换框架与归结模式合一算法，以构造反驳并提取表示 Herbrand 相继式的 Herbrand 模式。
2024-04-09 math.LO
On Natural Deduction for Herbrand Constructive Logics II: Curry-Howard Correspondence for Markov's Principle in First-Order Logic and Arithmetic
直觉主义一阶逻辑用马尔可夫原理的一个限制形式扩展是构造性的，并承认Curry-Howard对应，如Herbelin所示。我们提供了一个更简单的证明结果，然后我们研究直觉一阶逻辑扩展的无限制马尔可夫原理。从经典自然演绎出发，对排中律进行了限制，得到了一个自然演绎系统和一个平行的Curry-Howard同构。我们证明存在量化公式的证明项减少到代表所有可能证人的单个项的列表。作为推论，我们得出该逻辑是Herbrand构造性的：每当它证明任何存在公式时，它也证明该公式的Herbrand析取。最后，使用刚刚介绍的技术，我们还提供了一个新的计算解释的算术与马尔可夫的原则。
2017-10-17 cs.LO math.LO
Herbrand's theorem and non-Euclidean geometry
利用Herbrand定理给出了一个新的证明，证明了欧几里德的平行公理不能从一阶欧几里德几何的其它公理导出。以前的证明涉及构建非欧几里德几何模型。这个证明使用了一个非常古老的基本逻辑定理，以及一些简单的性质的标尺和指南针结构，以给出一个简短，简单，直观的证明。
2015-02-23 math.LO
On the Herbrand content of LK
我们提出了一个结构表示的Herbrand内容的LK证明与削减的复杂性prenex Sigma-2/Pi-2。该表示采取的形式，一个类型的非确定性树文法的顺序2生成一个有限的语言的一阶项出现在Herbrand扩展通过削减消除。特别是，对于每一个根岑风格的减少之间的LK证明，我们研究的诱导语法和分类的情况下，语言平等和包容举行。
2016-06-21 cs.FL cs.LO math.LO
The Epsilon Calculus and Herbrand Complexity
希尔伯特的ε演算是基于谓词逻辑语言的扩展，通过一个项形成算子$ε_{x}$。关于ε-演算的两个基本结果，第一和第二ε-定理，起着类似于切消定理在ε-演算中所起的作用。特别是，赫布兰德定理是一个后果，该定理。本文研究了存在性定理和消除程序的复杂性，以及通过这种消除程序获得的存在性定理的Herbrand析取的长度。
2005-10-28 math.LO
Herbrand's Fundamental Theorem - an encyclopedia article
Herbrand基本定理用谓词逻辑的方法构造性地刻画了一阶谓词逻辑的可导性。有时它只是所谓的“Herbrand定理”，但较长的名称是可取的，因为还有其他重要的“Herbrand定理”和Herbrand本人称之为“Theorème fondamental”。Bernays [1957]对它的排名如下：“在它的证明论形式中，Herbrand定理可以被看作是谓词逻辑的中心定理。它以一种简洁而恰当的形式表达了谓词逻辑与命题逻辑的关系。海杰努特（Heijenoort，1967）说：“让我简单地说，在结论中，Begriffsschrift（Frege，1879），Löwenheim的论文（1915）和Herbrand论文（1930）的第五章是现代逻辑的三个基石。Herbrand的基本定理出现在他的博士论文[1930年]的第5章-题为Recherches sur la théorie de la démonstration -由Jacques Herbrand（1908-1931）于1929年在巴黎大学提交。赫布兰德基本定理与哥德尔不完备性定理和根岑的Hauptstern定理一起，是现代逻辑中最有影响力的定理之一。由于其复杂性，赫布兰德基本定理在教科书中通常被搞得面目全非。由于我们相信，这个定理还有很多东西需要学习，比许多逻辑学家所知道的要多得多，我们将把重点放在真正的信息及其实际影响上。这需要…
2015-03-04 math.LO
Existential completions and Herbrand's theorem
本文通过构造分配格预层上的自由存在完备化，给出相干逻辑 Herbrand 定理的更直接代数证明，并讨论交半格预层与 frame 预层情形。
2025-08-21 math.CT math.LO
Schematic Cut elimination and the Ordered Pigeonhole Principle [Extended Version]
在以前的工作中，尝试将示意CERES方法[8]应用于具有任意数量的N2切割的形式证明（封装无限鸽子洞原理的递归证明）[5]。然而，对证明的特征子句集的推导的图解反驳不能用[8]中提供的形式语言表达。如果没有这种形式化，就不能用算法提取Herbrand系统。本文对文[5]中的证明给出了一个限制，即ECA-模式（最终常数断言）或有序无穷鸽子洞原理，其分析完全可以在文[8]的框架中进行，这是首次将该框架用于证明分析。从子句集的反驳和替换图式出发，我们构造了一个Herbrand系统。
2016-01-25 cs.LO math.LO
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 Nets, Coends and the Yoneda Isomorphism
证明网提供置换无关的证明表示，并用于研究monoidal范畴的一致性问题。研究了二阶乘法线性逻辑（MLL2）的一个一致性问题，即用端和余端刻画量词解释所生成的证明的等价性问题.我们提供了一个紧凑的表示证明网MLL2相关的米田同构的片段。通过调整“重新布线的方法”中使用的一致性结果的明星自治类别，我们定义了一个等价关系的证明网称为“重新见证”。我们证明，这种关系的特点，在这个片段中，产生的等价coends。
2019-04-15 cs.LO math.LO
Proof Schemata for Theories equivalent to $PA$: on the Benefit of Conservative Reflection Principles
归纳通常形式化为LK演算的规则或公理扩展。虽然这种对微积分的扩展简单而优雅，但证明转换和分析可能相当困难。具有归纳规则的理论，例如皮亚诺算术，没有{ \em Herbrand}定理。在这项工作中，我们扩展了现有的元理论形式主义，所谓的证明图式，递归公式的归纳特别适合于证明分析，皮亚诺算术。这种关系在\PA和另一种证明形式主义之间提供了一个有意义的保守反射原则。证明图式已被证明有一个变种的Herbrand定理的经典逻辑，可以提升到我们的新的形式主义相当于原始的递归算术的子系统。
2018-04-01 math.LO
Abstract p-time proof nets for MALL: Conflict nets
本文提出了乘加线性逻辑（MALL）的证明网，称为冲突网。它们是有效的，因为证明的正确性和翻译都是p-时间（多项式时间），并且是抽象的，因为它们在转置相邻的&-规则下是不变的。一个抽象上的冲突网是简洁的：公理与冲突关系相联系。冲突网是最近为经典逻辑引入的组合证明的一个变体（并受到其启发）：每一个都可以被视为可收缩相干空间（P_4-free graphs，或cographs）的极大映射（同态），从公理到公理。本文给出了其他证明网的新结果：（1）切片网（Hughes/van Glabbeek 2003）的正确性和割消是p-时间的;（2）单项式网（Girard 1996）的割消不起作用。打破单项网割消的微妙之处也适用于冲突网：与单项网一样，合流割消的存在仍然是一个悬而未决的问题。
2008-01-16 math.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
Expansion Trees with Cut
赫布兰德定理是逻辑学中最基本的见解之一。从句法的角度来看，它建议一个紧凑的表示证明在经典的第一和高阶逻辑记录的信息，哪些实例已被选定的量词，在文献中称为扩展树。这样的表示本质上是解析的，因此对应于一个无割的微积分证明。最近几个扩展的证明表示证明与削减已被提出。这些扩展是基于类似于证明网的图形形式主义，并仅限于前束公式。在本文中，我们提出了一种新的方法，直接扩展扩展树的切割和覆盖也非前束公式。我们描述了一个削减消除程序，我们的扩展树削减是基于自然的减少步骤。我们证明，它是弱正规化使用的方法从ε演算。
2013-08-02 cs.LO math.LO
Proof nets and the instantiation overflow property
实例化溢出是那些二阶类型的属性，对于这些二阶类型，完全理解的所有实例都可以从原子理解的实例中推导出来。换句话说，当可以通过原子多态性键入实现应用于该类型的完整提取规则的实例的“扩展项”时，该类型具有实例化溢出。这一性质是在由著名的罗素-普拉维茨翻译逻辑连接词到系统F中所产生的类型的情况下进行研究的，但并不局限于这样的类型。此外，它可以与函子多态性有关，函子多态性是系统F中参数性的一种众所周知的范畴方法。在本文中，我们研究的实例溢出性质，利用表示的派生通过线性逻辑证明网。我们开发了一个几何的方法，实例化溢出产生更深入的理解的结构的扩展条款和拉塞尔-Prawitz类型。我们的主要结果是一类类型的形式$\forall XA$，其中$A$是一个简单的类型，它享有实例化溢出属性，通过推广的Russell-Prawitz类型的特征。
2018-03-25 cs.LO math.LO
Herbrand Game Complexity
Univ. of California, San Diego（加州大学圣地亚哥分校）；Czech Academy of Sciences, Prague（捷克科学院）
研究纯一阶逻辑环境下学生-教师博弈的赫尔布兰德博弈复杂性，给出细化版本，证明其有效性。通过构造前束公式\(\varphi\)，表明该博弈最小树可能任意复杂，得出赫尔布兰德析取大小和复杂性均无界的结论。
2026-10-19 math.LO
Simple multiplicative proof nets with units
本文提出了一种简单的带单位乘法线性逻辑证明网的概念。削减消除是直接的和强烈的归一化，与以前的方法，采取移动跳跃（附件）的标准杆单位在归一化。证明网范畴中的复合只是路径复合：所有的动力学都发生在GoI（Setp）中，GoI（Setp）是应用于集合和部分函数的集范畴范畴的相互作用几何结构。
2005-07-01 math.CT math.LO
Proof nets for the Lambek calculus with one division and a negative-polarity modality for weakening
在本文中，我们介绍了一个变种的Lambek演算允许空的前件。这个变体使用两个连接词：左分裂和一元模态，只在负极性时出现，并允许弱化后继词的先行词。我们定义了这个演算的证明网的概念，这是类似于普通的Lambek演算和乘法线性逻辑。我们证明了一个图在所考虑的演算中是可导的当且仅当它存在一个证明网，从而我们建立了一个基于图的可导性准则.图的大小由图的长度限定。
2019-12-08 math.LO
Elimination and cut-elimination in multiplicative linear logic
我们将乘法线性逻辑中的每个证明结构与一个理想相关联，该理想将证明的逻辑内容表示为多项式方程。我们展示了如何削减消除乘法证明网对应的Buchberger算法的实例计算Gröbner基地消除理论。
2022-07-22 cs.LO math.LO
Expansion Trees with Cut
赫布兰德定理是逻辑学中最基本的见解之一。从句法的角度来看，它建议在经典的一阶和高阶逻辑的证明的紧凑表示记录的信息，哪些实例已被选择的量词。这种紧凑的表示在文献中被称为米勒扩展树证明。它本质上是解析的，因此对应于一个无割集演算证明。最近，人们提出了将这种证明表示扩展到具有切割的证明的几种扩展。这些扩展是基于类似于证明网的图形形式主义，并仅限于前束公式。在本文中，我们提出了一个新的句法方法，直接扩展米勒的扩展树的切割和覆盖也非前旋公式。我们描述了一个削减消除程序，我们的扩展树削减是基于自然的减少步骤，并表明它是弱正规化。
2018-02-21 math.LO
Classical Logic = Fibred MLL
本文将经典的命题证明表示为 * 组合证明 *，这比证明网更抽象：叠加（收缩/弱化）在数学上被建模为纤维化的松散形式，而不是语法（如在证明网中，涉及收缩和弱化节点）。一个组合证明是一个“被证明的”乘法线性证明网，因此标题中的口号。割消法保留了它来自微积分的丰富性：它的非决定性不会崩溃而成为融合。[Note：这仅仅是一个2页的概要，接受在计算机科学逻辑'05的简短介绍。
2005-04-01 math.LO
Skolemization In Intermediate Logics
本文刻画了允许标准及Andrews Skolem化的中间一阶逻辑，并为其他逻辑开发新型Skolem函数，同时证明带量词移位公理的谓词直觉主义逻辑的Kripke框架不完全性，以促进非经典逻辑的消解式定理证明。
2025-01-26 cs.LO math.LO
Constructive proofs for the standard translation of many-sorted to unsorted predicate logic
Institut für Philosophie I, Ruhr-Universität Bochum（波鸿鲁尔大学哲学研究所）
本文研究了多排序逻辑到无排序一阶逻辑的翻译问题，提出了一种有效的构造性证明方法，解决了现有证明在包含等价关系时的不足，并给出了van Dalen将二阶逻辑翻译为无排序一阶逻辑的完全语法证明。
2026-05-17 math.LO
Linear Logic and Quantum Error Correcting Codes
本文提出基于量子纠错码的乘法证明网归约新视角，将每个证明网关联一个码，使割消去等价于纠错过程。
2024-05-29 math.LO quant-ph
Coherence of Proof-Net Categories
本文定义的证明网范畴的概念与线性逻辑中无常数命题的乘法片段的证明网中隐含的图密切相关。类似的图形出现在凯利和麦克莱恩的相干定理对称monoidal闭范畴。证明了证明网范畴的相干定理。这种一致性定理也证明了相应的线性逻辑的混合原则的箭头的存在。证明网范畴的概念抓住了星自治范畴概念的单位自由片段，星自治范畴是一类特殊的对称monoidal闭范畴。
2005-10-04 math.CT math.LO
Material Interpretation and Constructive Analysis of Maximal Ideals in $\mathbb{Z}[X]$
本文提出物理解释方法，通过将经典蕴含转化为构造性析取，以 $\mathbb{Z}[X]$ 中极大理想为例给出构造性证明，揭示计算内容并探讨其在多个经典引理及算法实现中的应用。
2025-04-10 math.AC math.LO
