Cut-restriction: from cuts to analytic cuts
针对多数非经典逻辑相继式演算不满足切消定理的问题，提出切限制方法，将任意切割限制为解析切割，适用于满足易检条件的演算，统一涵盖现有结果并建立新的解析子公式性质。
2023-04-28 cs.LO
Cut-elimination and the decidability of reachability in alternating pushdown systems
给出了交替下推系统可达性判定的一个新的证明，证明了它是某些自然演绎推理系统的割消定理的一个简单推论。然后，我们展示了如何使用这个结果可以扩展到一个完整的系统，为每一个配置$A$，无论是$A$或$\neg A$是可证明的交替下推系统。
2014-10-30 cs.LO
Axioms vs. rewrite rules: from completeness to cut elimination
本文研究自动定理证明中证明搜索与重写结合时的完备性问题，指出其关键在于为演绎与计算结合的扩展证明概念建立切割消去，从而揭示自动定理证明与证明论之间的新联系。
2023-06-01 cs.LO
On the cut-elimination of the modal $μ$-calculus: Linear Logic to the rescue
本文借助线性逻辑及其指数模态构造线性化系统 \muLLmodinf{}，并通过线性翻译证明非良基模态 $μ$-演算的语形切割消除。
2025-06-11 cs.LO
Syntactic cut-elimination and backward proof-search for tense logic via linear nested sequents (Extended version)
本文给出了基本正规时态逻辑Kt的一个线性嵌套演算。我们表明，演算，使向后证明搜索，反模型建设和句法切割消除。因此，线性嵌套序列提供了为包含逆的模态逻辑提供足够的证明理论所需的最小嵌套量。作为奖励，这产生了对称模态逻辑KB的无切演算。
2019-07-02 cs.LO
A theory of cut-restriction: first steps
割消是证明理论的基础。正是这种算法消除了微积分证明中的切割，导致了无切割微积分和应用。割消适用于许多逻辑，而与它们的语义无关。这是它的影响，每当削减消除是不可证明的微积分不变的反应一直是一个移动到一个更丰富的证明系统，以恢复it.In本文中，我们调查了一个根本不同的方法，后者：适应古老的削减消除限制的形状时，消除是不可能的削减公式。我们解决了无割以上的“第一级”：分析割。我们的方法被应用到双直觉逻辑和S5的分析削减已经知道是必需的微积分。这标志着切割限制理论的第一步。
2022-03-03 cs.LO
IMELL Cut Elimination with Linear Overhead
本研究针对直觉主义乘法指数线性逻辑的切消问题，为指数替换演算引入抽象机，完善了已有结果，证明该机器实现好策略且能在线性开销内得到无切证明。
2024-05-14 cs.LO
Fast Cut-Elimination using Proof Terms: An Empirical Study
Urban和Bierman引入了一个演算的证明项的演算LK与一个强正规化的约简关系。我们将这种演算扩展到简单类型的高阶逻辑与归纳和等式的推论，尽管没有强规范化。我们实现thiscalculus在GAPT，我们的图书馆证明转换。评估人工和现实世界的基准上的归一化，我们表明，该算法通常是几个数量级的速度比现有的Gentzen样削减减少，和一个数量级的速度比任何其他削减消除程序中实现的GAPT。
2018-10-17 cs.LO
Syntactic Cut-Elimination for Provability Logic GL via Nested Sequents
本文针对可证性逻辑GL切割消去终止性证明困难的问题，提出基于嵌套矢列式的语法化切割消去方法，并借鉴Kushida（2020）的思想，仅用直接归纳避免额外度量和复杂重写，从而消除Poggiolesi（2009）证明中的歧义。
2024-12-31 cs.LO
Elimination and cut-elimination in multiplicative linear logic
我们将乘法线性逻辑中的每个证明结构与一个理想相关联，该理想将证明的逻辑内容表示为多项式方程。我们展示了如何削减消除乘法证明网对应的Buchberger算法的实例计算Gröbner基地消除理论。
2022-07-22 cs.LO math.LO
Infinitary Cut-Elimination for Non-Wellfounded Parsimonious Linear Logic
本文研究节俭线性逻辑的非良基证明系统，提出基于有限逼近的无穷消切，证明其在进展准则下产生良定义证明并保持正则性，且给出关系模型指称语义。
2025-09-01 cs.LO
A uniform cut-elimination theorem for linear logics with fixed points and super exponentials
针对轻量线性逻辑变体切消定理证明冗余的问题，结合归约翻译法与充分条件判定法，为带不动点的参数化线性逻辑系统提出统一切消定理，覆盖多类指数联结词系统。
2025-06-17 cs.LO
Making progress: Reducibility Candidates and Cut Elimination in the Ill-founded Realm
本文提出两种基于可约候选者技术的非良基μMALL切消论证，通过定义性质保证进步性，利用拓扑内部闭集概念完成第二个论证。
2026-02-13 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
Cut Elimination for a Logic with Induction and Co-induction
证明搜索已被用于指定广泛的计算系统。为了建立一个框架，这样的规范推理，我们使用了一个微积分，涉及感应和共感应。这些证明原则是基于定义的证明理论（而不是集合论）概念。定义类似于逻辑程序，其中定义原子的左规则和右规则允许人们将理论视为“封闭的”或定义不动点。定义和自由相等的使用使得有意识地推理语法成为可能。我们以一致的方式添加规则前和后固定点，从而允许用户的原因归纳和共归纳的计算系统的属性，充分利用高阶抽象语法。一致性是保证通过削减消除，在那里，我们给第一，据我们所知，削减消除程序存在的一般归纳和共归纳的定义。
2010-09-30 cs.LO
On the Cut Elimination of Weak Intuitionistic Tense Logic
本文提出一种通过分裂收缩规则和切割规则来证明弱直觉时态逻辑切割消去的新方法，并展望其未来理论扩展与应用。
2024-05-27 cs.LO math.LO
The Cut Elimination and the Nonlengthening Property for the Sequent Calculus with Equality
我们展示了Leibnitz的不变性原理和Gentzen的原始工作是如何将微积分推广到具有等式的一阶逻辑的，并研究了割消性质。进一步讨论并改进了Lifshitz和Orevkov的不伸长性.
2017-05-01 cs.LO math.LO
The failure of cut-elimination in cyclic proof for first-order logic with inductive definitions
本文证明带归纳定义的一阶逻辑循环证明系统中切割消除不成立，通过构造一个必须依赖切割规则才能证明的相继式实例，证实了该系统无法消除切割的猜想。
2024-02-15 cs.LO math.LO
Cut elimination for Cyclic Proofs: A Case Study in Temporal Logic
University of Gothenburg（哥德堡大学）；University of Amsterdam（阿姆斯特丹大学）
本文为扩展了“最终”时序算子的模态逻辑的循环矢列演算提供切消过程，将归约切消方法适配至循环演算，能直接将循环证明转化为无切循环证明而无需正则化机制。
2025-11-04 cs.LO math.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
Conservativity for theories of compositional truth via cut elimination
我们提出了一个削减消除的论点，见证了保守性的组成公理的真理（没有扩展归纳公理）在任何理论解释一个薄弱的算术子系统。在这样做的时候，我们还修复了Halbach原始演示文稿中的一个关键错误。我们的方法表明，这些公理的录取决定了超指数减少的大小推导的真实自由的声明。
2013-08-01 cs.LO math.LO
Cut Elimination for a Logic with Generic Judgments and Induction
本文给出了逻辑$LG^ω$的割消证明，它是Miller和Tiu的逻辑$\FOLDNb$的一般判断编码证明系统的推广，并采用归纳法原理.逻辑$LG^ω$，就像$\FOLDNb$一样，以一阶直觉逻辑的扩展为特征，具有不动点和"通用量词“$\nabla$，用于推理逻辑中编码的对象系统中绑定的动态。以前尝试用归纳原则扩展$\FOLDNb$，但在归纳规范中对绑定的某些行为进行建模时没有成功。事实证明，这个问题可以通过放松对$\nabla$的一些限制来解决，特别是通过添加公理$B \equiv \nabla x. B$，其中$x$在$B$中不是自由的。我们表明，通过采用等方差原理，表示的扩展逻辑可以大大简化。本文包含\cite{tiu07entcs}中所述结果的技术证明;鼓励读者查阅\cite{tiu07entcs}以了解$LG^ω.$的动机和示例
2008-01-20 cs.LO
A new calculus for intuitionistic Strong Löb logic: strong termination and cut-elimination, formalised
本文为直觉主义强Löb逻辑提出新相继式演算，实现强终止的向后搜索与句法消割，并在Coq中形式化验证。
2023-09-01 cs.LO math.LO
Cut elimination for the alternation-free modal mu-calculus
University of Gothenburg（哥德堡大学）；University of Amsterdam（阿姆斯特丹大学）
本文为模态μ-演算的无交替片段提出一种基于循环证明系统的语法切消去过程，利用多切和良拟序理论直接将带切证明转换为无切证明并保证终止。
2026-10-23 cs.LO math.LO
Semantic A-translation and Super-consistency entail Classical Cut Elimination
我们证明了，如果由重写系统定义的理论R是超相容的，则经典的模R演算具有割消性质，这是一个公开的问题。对于这样的理论，我们已经知道，证明在模R的自然演绎中是强规范化的，而切消在模R的直觉主义微积分中是成立的。我们首先定义一个语法和语义版本的弗里德曼的A-翻译，表明它保留了伪海廷代数，我们的语义框架的结构。然后，我们将理论在A-平移代数中的解释与它在原代数中的A-平移联系起来。这允许显示的超一致性准则和削减消除定理的稳定性。
2014-01-06 cs.LO math.LO
Compression for Coinductive Rewriting and the Cut-Elimination of Non-Wellfounded Proofs
Université Paris Cité（巴黎西岱大学）；CNRS（法国国家科学研究中心）；IRIF（IRIF实验室）；DISI, Università di Bologna（博洛尼亚大学DISI）；INRIA Picube
本文提出了一种通用方法，用于处理混合归纳与共归纳的语法对象，应用于无穷重构及非非良好基础证明的切消。
2026-08-24 cs.LO
Clausal Analysis of First-order Proof Schemata
证明图式是LK-证明的一种变体，能够通过向标准的一阶LK-演算添加所谓的证明链接来模拟一阶逻辑中的各种归纳方案。证明链接允许证明引用证明，从而为证明模式提供递归结构。不幸的是，在存在证明链接的情况下，应用约简割消是不平凡的。借用函数式编程中的惰性实例化的概念，我们在本地评估证明链接，允许还原切割消除进行过去。虽然，这种方法不能被用来获得切割自由证明模式，我们仍然获得了重要的结果，示意CERES方法，即切割消除证明模式的基础上的决议。在“Towards a clausal analysis of cut-elimination”一文中，我们指出，约简割消变换了一个给定的LK-证明，使得变换前后的特征子句集（即表示一个LK-证明的割结构的子句集）之间存在一个包含关系。设CL（A '）是一个LK-证明A的范式A'的特征子句集，该范式A '是通过对A进行约化割消元而不进行原子割消元得到的。则CL（A '）被从对A的任何约化割消应用中提取的所有特征小句集合所包含。这种范式被称为ACNF top，在通过分解消除割的方法中起着重要作用。这些结果可以通过我们的证明链接的“惰性实例化”推广到证明模式，并且为证明模式的完全切消元法提供了必要的一步。
2017-02-08 cs.LO math.LO
A study of cut-elimination for a non-labelled cyclic proof system for propositional dynamic logics
Graduate School of Information Sciences, Tohoku University（东北大学信息科学研究院）
本文研究了命题动态逻辑中非标记循环证明系统的消去问题，提出了序数演算和循环证明系统，并证明了其正确性和完备性，同时展示了消去失败及限制后的消去性质。
2026-03-02 cs.LO math.LO
Cut elimination for Zermelo set theory
本文通过将策梅洛集合论重构为指向图理论并将公理转化为重写规则，在演绎模中实现了其直觉主义片段的正规化，并证明了所得理论是原集合论的保守扩张。
2023-10-31 cs.LO
A Constructive Proof of Cut Elimination for a System of Full Second Order Logic
本文给出了一个完全二阶逻辑系统的割消的构造性证明，它吸收了结构规则，用集合代替序列。通过使用一个新的诱导参数，cutrank增长的标准问题是避免。这种技术也可以应用于一阶逻辑。
2016-06-21 cs.LO math.LO
Exponentials as Substitutions and the Cost of Cut Elimination in Linear Logic
本文提出指数替换演算（ESC），基于显式替换思想为IMELL切割消除提供新表示，设计了具有子项性质的切割消除策略，首次为无约束指数的切割消除提供多项式代价模型，并证明了无类型合流与有类型强规范化。
2023-12-13 cs.LO cs.PL
A study for recovering the cut-elimination property in cyclic proof systems by restricting the arity of inductive predicates
本文研究循环证明系统中消切性质失效的原因，证明即使将语言限制为一元归纳谓词和一元函数，消切性质在简单循环证明系统中仍不成立，改进了先前需三元谓词的反例。
2025-03-05 cs.LO math.LO
Syntactic Cut-Elimination for Intuitionistic Fuzzy Logic via Linear Nested Sequents
本文利用线性嵌套框架设计了一种新的直觉模糊逻辑--一阶Gödel逻辑的无割演算LNIF。线性嵌套序列-这是嵌套序列限制线性结构-证明是一个很好的证明理论的形式主义直觉模糊逻辑。我们发现，演算LNIF具有非常理想的证明理论的性质，如可逆的所有规则，结构规则的容许性，和句法切割消除。
2020-10-04 cs.LO math.LO
Inducing syntactic cut-elimination for indexed nested sequents
本文通过建立标记相继式与索引嵌套相继式的对应关系，为索引嵌套相继式演算引入句法切割消去证明，并首次为中间逻辑构造了无切割的索引嵌套相继式演算。
2018-11-23 cs.LO
The problem of Pi_2-cut-introduction
本文提出了一种基于Pi_2-割的无割LK-证明压缩算法。本文的方法是基于Gentzen割消法的一个逆，推广了以往引入Pi_1-割的方法。Herbrand实例的削减免费证明pi的一个CNORS描述的语法G编码的替代定义在消除量化削减。本文给出了一个算法，它在给定文法G的情况下，构造了一个Pi_2-割公式A，并证明了S在A上有一个割.结果表明，通过该算法，我们可以实现指数证明压缩。
2018-01-15 cs.LO
Cut elimination for propositional cyclic proof systems with fixed-point operators
本文研究带不动点算子或归纳定义的命题循环证明系统，证明其与无穷式系统可证明性等价，并因此具有无切割完备性。
2024-10-29 cs.LO math.LO
Semantic Cut Elimination for the Logic of Bunched Implications, Formalized in Coq
集束蕴涵逻辑（BI）是构成分离逻辑主干的子结构逻辑，分离逻辑是研究堆操作程序推理的逻辑。虽然BI的证明理论和元理论在数学上都有涉及，但重要的元理论结果的形式化仍然刚刚起步。在本文中，我们提出了一个自包含的形式化，在Coq的证明助手，证明了中央元理论性质的BI：削减消除其微积分。提出的证明是 * 语义 *，在这个意义上说，是通过解释在一个特定的“通用”模型的序列。这导致了一个比标准的Gentzen风格的切割消除参数更模块化和优雅的证明，这在BI的手动证明中可能是微妙和容易出错的。特别是，我们的语义方法避免了不必要的反演证明推导，或使用削减减少和多削减规则。除了模块化，我们的方法也是强大的：我们演示了我们的方法规模，与微小的修改，（i）BI的扩展与任意一组的\emph{simple structural rules}，和（ii）扩展与S4一样的$\Box$模态。
2021-12-10 cs.LO math.LO
Topological Observations on Multiplicative Additive Linear Logic
作为一种尝试，以揭示的拓扑性质的组合策略的游戏语义，我们提出了一个“拓扑”的游戏乘加线性逻辑没有命题变量，包括削减移动。我们重铸的概念（获胜）的战略和削减消除在这种情况下的问题，并证明削减消除定理。最后，我们证明了可靠性和完备性。拓扑结构起着至关重要的作用，特别是通过策略形成一个层的事实。
2008-07-14 cs.LO
Cut-Elimination and Proof Search for Bi-Intuitionistic Tense Logic
我们考虑了双直觉逻辑与时态逻辑Kt的传统模态的扩展。从理论上证明，这种扩展是简单地通过扩展现有的双直觉逻辑的演算与显示逻辑中使用的模态的典型推理规则。事实证明，由此产生的演算LBiKt似乎比文献中考虑的大多数直觉时态或模态逻辑更基本，特别是Ewald和Simpson研究的那些，因为它没有假设菱形和盒子模态算子之间的任何先验关系。我们恢复Ewald的直觉时态逻辑和Simpson的直觉模态逻辑的模块化扩展LBiKt与额外的结构规则。演算LBiKt是以显示演算的一种变体形式来公式化的，使用一种称为嵌套序列的序列形式。切割消除证明LBiKt，使用类似的技术，在显示结石。与显示演算一样，LBiKt的推理规则是“浅”规则，也就是说它们作用于嵌套表达式中的顶级公式。演算LBiKt不适合向后证明搜索，因为存在某些称为“显示假设”的结构规则和任意结构上的压缩规则。我们表明，这些结构规则可以在另一个演算，DBiKt，它使用深度推理，允许一个应用推理规则在任意深度的嵌套的嵌套的。我们证明了LBiKt和DBiKt之间的等价性，并概述了DBiKt的证明搜索策略。我们还给出了一个Kripke语义，并证明了LBiKt是健全的语义，但完整性仍然是一个开放的问题。然后我们讨论LBiKt的各种扩展。
2010-06-29 cs.LO
A MALL Geometry of Interaction Based on Indexed Linear Logic
本文为乘法-加法线性逻辑构建基于索引线性逻辑的交互几何，扩展了Haghverdi-Scott范畴框架，利用索引处理加法消割的叠加、擦除和收缩，并证明执行公式沿消割不变，收敛到无割证明的指称。
2020-07-28 cs.LO
MacNeille completion and Buchholz' Omega rule for parameter-free second order logics
Buchholz'Omega-规则是一种给出二阶算术的各种子系统的割消的句法的、可能无序的证明的方法。我们的目标是从代数的角度来理解它。在高阶逻辑的割消的许多证明中，Maehara和Okada的代数证明特别有趣，因为他们的论点的本质可以用代数描述为（Dedekind-）MacNeille完成与Girard的约化候选人。有趣的是，事实证明，作为逻辑推理规则的$Ω$规则在MacNeille完备化中找到了其代数基础。在本文中，我们考虑无参数片段LIP 0，LIP 1，LIP 2，…二阶直觉主义逻辑，对应于算术理论ID 0，ID 1，ID 2，.迭代归纳的定义直到Ω。在这种情况下，我们观察到欧米茄规则和MacNeille完成之间的正式连接，导致一种解释二阶量词在一阶的方式在Heyting值的语义，称为欧米茄解释。在此基础上，给出了LIPn的割消的代数证明，证明了LIPn的割消在IDn中是局部形式化的.作为一个结果，我们得到了LIPn的切割消除和IDn的1-一致性之间的等价性，在弱算术理论中成立。
2019-04-09 cs.LO
CERES for First-Order Schemata
割消法CERES（用于一阶和高阶经典逻辑）是基于特征子句集的概念，它是从LK证明中提取出来的，并且总是不可满足的。这个子句集的归结反驳可以用作仅使用原子割（原子割范式）的证明的框架。这是通过用原始证明的相应投影替换归结反驳中的子句来实现的。我们提出了一个概括的CERES（称为CERES）的一阶证明图式，并定义了一个示意性版本的微积分称为LKS，和原始递归定义的基础上证明模式的概念。提出了一种从这些证明图式中提取图式特征子句集和图式投影的方法。我们还定义了一个用于反驳小句集图式的图式归结演算，它可以用来反驳图式特征小句集。最后将投影图式和分辨图式连接起来，得到了原子割范式的一个图示。CERES的一个主要好处是削减消除归纳定义的证据的延伸：我们比较CERES与标准结石使用归纳规则，并证明CERES是能够执行削减消除传统方法失败。CERES的算法处理得到CERES系统最近扩展的支持。
2013-03-18 cs.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
Propositions in Linear Multirole Logic as Multiparty Session Types
我们确定多角色逻辑作为一种新形式的逻辑和形式化线性多角色逻辑（LMRL）作为一个自然的推广经典线性逻辑（CLL）。在为LMRL建立的各种元性质中，我们得到了一个称为多割消去的元性质，即三个（或更多）序列之间的每一个割（作为两个序列之间的割的推广）都可以消去，从而推广了Gentzen关于割消去的著名结果.我们还提出了一个变体的$π$ -演算的多方会话，证明了一个紧密的对应关系，在这个变体的过程中的通信和多割消除LMRL，从而扩展了Caires和Pfenning（2010）和Wadler（2012）的一些最近的结果，以及其他类似的工作。
2016-11-27 cs.LO cs.PL
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
Generalised Proof-Nets for Compact Categories with Biproducts
正如传统的函数程序可以被理解为直觉主义逻辑中的证明一样，量子过程也可以被视为合适逻辑中的证明。我们描述这样一个逻辑，紧凑的闭范畴和biproducts的逻辑，提出了作为一个微积分和作为一个系统的证明网。这种逻辑捕捉了在经典控制下表示量子过程所需的大部分必要结构，同时对细节保持不可知论。我们演示了如何表示量子过程的证明网，并表明量子过程的动态行为被捕获的逻辑的削减消除过程。我们表明，削减消除程序是强烈规范化：也就是说，每一个法律的简化证明网络的方式导致相同的，唯一的，正常的形式。最后，采取一些初始的操作作为非逻辑公理，我们表明，由此产生的类别的证明网是一个表示的自由紧凑的闭范畴与这些操作所产生的双产品。
2009-03-30 cs.LO math.CT
Subatomic Proof Systems: Splittable Systems
本文介绍了第一个一系列的结果，使我们能够开发一个理论，提供更精细的控制的复杂性的规范化，特别是削减消除。通过把原子看作是自对偶的非交换连接词，我们能够以一种统一的、非常简单的方式对大量的推理规则进行分类。这使我们能够定义简单的条件，这些条件很容易验证，并通过一般定理确保归一化和切割消除。在本文中，我们定义和考虑可分裂系统，它基本上包括一个大类的线性逻辑，包括MLL和BV，我们证明了他们的分裂定理，保证削减消除和其他容许结果的推论。在接下来的论文中，我们将把这个结果推广到非线性逻辑。最终的结果将是一个全面的理论，为大多数现有的逻辑提供统一的处理，并为未来的证明系统的设计提供蓝图。
2017-12-04 cs.LO
The Structure of Differential Invariants and Differential Cut Elimination
混合系统验证的最大挑战是微分方程的处理。由于可计算的封闭形式的解决方案只存在于非常简单的微分方程，证明证书已经提出了更可扩展的验证。然而，这些证明证书的搜索过程仍然是相当特殊的，因为对问题结构的理解很差。我们研究微分不变量，它定义了微分方程的归纳原理，并且可以通过使用它们的微分结构来检查微分方程的不变性，而不必求解它们。研究了微分不变量的结构性质。为了分析证明搜索复杂性的权衡，我们确定了几类微分不变量之间的十几种关系，并比较了它们的演绎能力。作为我们的主要结果，我们分析了微分割的演绎能力和带有辅助微分变量的微分不变量的演绎能力。我们反驳了差分切割消除假设，并表明，与标准切割，差分切割的基本证明原则，严格增加了演绎能力。我们还证明了演绎能力进一步增加时，添加辅助微分变量的动态。
2012-11-23 cs.LO math.CA math.DS
Proof nets for Herbrand's Theorem
本文探讨了经典逻辑证明论的两个中心结果：根森的微积分割消与赫布兰德的“基本定理”之间的联系。本文从Herbrand定理的一种高度结构化的表达方式Miller的扩展树证明出发，定义了一阶经典逻辑的无弱化证明网演算，并给出了一个弱规范化割消过程。在这种演算中，不可能对割消的汇合给出通常的反例，但它仍然是不汇合的，这使人们相信经典逻辑本质上是不汇合的。
2010-05-21 cs.LO math.LO
Super Exponentials in Linear Logic
根据次指数线性逻辑和分层有界线性逻辑的思想，我们提出了一个新的参数化版本的线性逻辑，它包含其他系统，如ELL，LLL或SLL，包括指数规则的变体。我们称这种系统为超指数线性逻辑（Superexponential Linear Logic，superLL）。通过对superLL的参数进行适当的约束，给出了割消元的一般性证明。这意味着线性逻辑的每一个变体，作为superLL的有效实例出现，也满足割消。
2021-12-30 cs.LO
Algorithmic Introduction of Quantified Cuts
本文描述了一种将经典一阶逻辑中的根岑割消法反演的方法。我们的算法是基于第一computign压缩表示的条款中存在的切割免费的证明，然后切割公式，实现这样的压缩。最后，使用这些切割公式的证明。该方法允许证明长度的指数压缩。它可以应用于自动定理证明器的输出，通常会产生分析证明。一个实现是在网络上，并在本文中描述。
2014-01-17 cs.LO
Subatomic systems need not be subatomic
亚原子系统最近被引入来识别支撑证明标准化的结构原则。“亚原子”意味着我们可以根据两个原则重新制定逻辑系统。它们的原子公式成为子原子的实例，逻辑常数之间的非交换自对偶关系，它们的规则可以通过一种独特的演绎方案，即中间形状推导出来。结果之一是，亚原子系统的割消意味着我们可以用亚原子表示的每个标准系统的割消。我们在这里介绍亚原子系统-1.1。他们放宽和拓宽了亚原子系统的子原子可以满足的性质，同时保持使用中间形状作为他们唯一的推理原则。由于亚原子可以直接操作变量，我们引入P。切消除P是切消除的推论，我们证明了亚原子系统-1.1。此外，P是健全的和完整的关于克隆在顶部的波斯特格。即P证明了所有且仅证明了包含合取、析取和投影的重言式。因此，P扩展了命题逻辑，而没有将其原子编码为P的子原子。这表明支撑亚原子系统的逻辑原则也适用于它们被设想工作的亚原子水平之外。我们通过引入内侧形状的集合R来加强这一观点。R中的规则所处理的公式属于Post格的两个不相交克隆的并。第一个克隆的SAT问题是在P时间。另一个的SAT问题是NP时间完全的。因此，R和亚原子系统的证明技术可以帮助识别从P-时间到NP-时间完全可满足性的相变的证明理论性质。
2018-04-22 cs.LO
Nested Sequents for Intuitionistic Multi-Modal Logics: Cut-Elimination and Lyndon Interpolation
本文提出了一种单结论嵌套序列表演算，用于直觉多模逻辑，并证明了切消性和Lyndon插值性质。
2025-11-27 cs.LO math.LO
CERES in Propositional Proof Schemata
割消是证明论中最著名的问题之一，根森在他著名的Hauptstern中定义并解决了一阶微积分中的割消问题。Ceres是一种不同的切割消除算法，用于一阶和高阶经典逻辑。Ceres被扩展到证明模式，这是通常的一阶证明的模板，带有自然数的参数。然而，虽然Ceres被认为是一阶逻辑的完全切割消除算法，但尚不清楚这是否也适用于一阶模式：在输入中给出一个带有切割的证明模式，Ceres总是产生一个无切割证明的模式吗？困难的一步是发现和表示一个适当的反驳模式的特征项模式的证明模式。在这篇论文中，我们在解决这个问题的进展限制谷神星命题图式，这是模板的命题证明。通过适当限制命题图式和证明图式的表达能力，我们的目标是提供一个版本的示意Ceres，这是一个完整的切割消除算法的命题图式。我们专注于谷神星的一个特定步骤：解决反驳图式。首先，我们证明，通过天真地适应Ceres的一阶模式，我们最终得到了一个不完整的算法。然后，我们稍微修改了归结反驳模式的概念：反驳一个子句集，首先我们把它带到一个通用的形式，然后我们使用一个固定的反驳该通用子句集。我们的变化的示意谷神星是第一步走向完整的命题图式。
2017-01-18 cs.LO math.LO
