Cut-elimination for the mu-calculus with one variable
我们建立了一个变量片段的模态μ演算的语法切割消除。我们的方法是基于最近的削减消除技术的薄荷糖，利用布赫霍尔茨的欧米茄规则。
2012-02-16 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
A Simple Proof That Super-Consistency Implies Cut Elimination
本文提出超一致性在模演绎中蕴含消切割的简化直接证明，并与涉及 V-复形的高阶逻辑定理比较。
2023-04-21 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
Cut-Elimination for the Bimodal Logic GR
Japan Coast Guard Academy（日本海上保安大学校）
本文提出GR双模逻辑的超序列演算，证明了切消定理。
2026-05-15 cs.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
A Constructive Proof of Cut Elimination for a System of Full Second Order Logic
本文给出了一个完全二阶逻辑系统的割消的构造性证明，它吸收了结构规则，用集合代替序列。通过使用一个新的诱导参数，cutrank增长的标准问题是避免。这种技术也可以应用于一阶逻辑。
2016-06-21 cs.LO math.LO
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
Cut Elimination in Multifocused Linear Logic
我们研究切消除的多焦点变体的全线性逻辑在微积分。多焦点范式的证明产生的问题，不出现在一个标准的聚焦系统，有关的限制，在分组规则的情况下，在聚焦阶段。我们表明，削减消除可以在一个明智的方式，即使证明需要一些特定的引理来处理多聚焦阶段，并讨论与削减消除时所产生的困难，考虑范式的证明在线性逻辑。
2015-02-17 cs.LO
Syntactic Cut-Elimination for Intuitionistic Fuzzy Logic via Linear Nested Sequents
本文利用线性嵌套框架设计了一种新的直觉模糊逻辑--一阶Gödel逻辑的无割演算LNIF。线性嵌套序列-这是嵌套序列限制线性结构-证明是一个很好的证明理论的形式主义直觉模糊逻辑。我们发现，演算LNIF具有非常理想的证明理论的性质，如可逆的所有规则，结构规则的容许性，和句法切割消除。
2020-10-04 cs.LO math.LO
Generic Modal Cut Elimination Applied to Conditional Logics
我们开发了一个通用的标准，削减消除命题模态逻辑，这取决于吸收削减，收缩，削弱和反演的纯模态部分的规则系统。我们的标准也适用于正常模态逻辑领域之外的各种逻辑。我们给我们的框架，以各种条件逻辑广泛的例子实例。对于这些，我们得到完全内化的结石，这是大大简单的比那些已知的文献中，随着精简证明削减消除和复杂性。在一种情况下，条件逻辑与肯定前件和条件排中律，削减消除和复杂性明确表示为开放的文献。
2011-03-17 cs.LO
Confluence as a cut elimination property
本文比较重写系统的合流性与证明论的切消概念，证明项重写系统的合流性质等价于其关联逻辑系统的切消性质，但该等价性不适用于直接重写原子命题的系统。
2023-05-23 cs.LO
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
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
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
Exponentials as Substitutions and the Cost of Cut Elimination in Linear Logic
本文提出指数替换演算（ESC），基于显式替换思想为IMELL切割消除提供新表示，设计了具有子项性质的切割消除策略，首次为无约束指数的切割消除提供多项式代价模型，并证明了无类型合流与有类型强规范化。
2023-12-13 cs.LO cs.PL
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
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
Proof nets for Herbrand's Theorem
本文探讨了经典逻辑证明论的两个中心结果：根森的微积分割消与赫布兰德的“基本定理”之间的联系。本文从Herbrand定理的一种高度结构化的表达方式Miller的扩展树证明出发，定义了一阶经典逻辑的无弱化证明网演算，并给出了一个弱规范化割消过程。在这种演算中，不可能对割消的汇合给出通常的反例，但它仍然是不汇合的，这使人们相信经典逻辑本质上是不汇合的。
2010-05-21 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
Differential Elimination and Algebraic Invariants of Polynomial Dynamical Systems
Two Six Technologies；Carnegie Mellon University（卡内基梅隆大学）；Karlsruhe Institute of Technology（卡尔斯鲁厄理工学院）
本文提出利用Rosenfeld-Gröbner算法获取多项式动力系统的代数不变量，避免使用Gröbner基和量化消除，通过识别全实变种提高不变性检查效率。
2026-04-01 cs.LO cs.SC math.AG
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
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
Cut elimination for Zermelo set theory
本文通过将策梅洛集合论重构为指向图理论并将公理转化为重写规则，在演绎模中实现了其直觉主义片段的正规化，并证明了所得理论是原集合论的保守扩张。
2023-10-31 cs.LO
A Semantic Proof of Generalised Cut Elimination for Deep Inference
本文提出一种语义方法，简洁证明深度推理系统MAV的广义消割性质，并在Agda中机械化证明，同时给出可靠性与完备性证明。
2024-12-07 cs.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
Nested Sequents for Intuitionistic Multi-Modal Logics: Cut-Elimination and Lyndon Interpolation
本文提出了一种单结论嵌套序列表演算，用于直觉多模逻辑，并证明了切消性和Lyndon插值性质。
2025-11-27 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
CERES in Propositional Proof Schemata
割消是证明论中最著名的问题之一，根森在他著名的Hauptstern中定义并解决了一阶微积分中的割消问题。Ceres是一种不同的切割消除算法，用于一阶和高阶经典逻辑。Ceres被扩展到证明模式，这是通常的一阶证明的模板，带有自然数的参数。然而，虽然Ceres被认为是一阶逻辑的完全切割消除算法，但尚不清楚这是否也适用于一阶模式：在输入中给出一个带有切割的证明模式，Ceres总是产生一个无切割证明的模式吗？困难的一步是发现和表示一个适当的反驳模式的特征项模式的证明模式。在这篇论文中，我们在解决这个问题的进展限制谷神星命题图式，这是模板的命题证明。通过适当限制命题图式和证明图式的表达能力，我们的目标是提供一个版本的示意Ceres，这是一个完整的切割消除算法的命题图式。我们专注于谷神星的一个特定步骤：解决反驳图式。首先，我们证明，通过天真地适应Ceres的一阶模式，我们最终得到了一个不完整的算法。然后，我们稍微修改了归结反驳模式的概念：反驳一个子句集，首先我们把它带到一个通用的形式，然后我们使用一个固定的反驳该通用子句集。我们的变化的示意谷神星是第一步走向完整的命题图式。
2017-01-18 cs.LO math.LO
Lattice Logic Properly Displayed
本文给出了（非分配）格逻辑的一个合理的、完备的、保守的、具有割消和子公式性质的显示演算。适当性（即在规则中所有参数部分的统一替换下的封闭性）是本提案的主要兴趣和附加值，并且允许最平滑的Belnap式切割消除证明。我们的建议建立在格逻辑的语义环境的代数和序理论的分析，并适用于显示演算的设计中的多类型的方法学的指导方针。
2016-12-18 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
The New Normal: We Cannot Eliminate Cuts in Coinductive Calculi, But We Can Explore Them
在微积分中，割消是一个保证任何可证明公式都可以被解析证明的属性。例如，根岑的经典和直观的演算LK和LJ享受削减消除。这个性质在微积分的余归纳扩张中研究得较少。在本文中，我们使用共归纳Horn子句理论，以证明切割是不可消除的共归纳扩展的LJ，一个系统，我们称之为CLJ。我们从这项研究中得出两个进一步的实际结果。我们表明，CoLP由古普塔等人。产生了削减免费证明CLJ与不动点条款，我们制定和实施一种新的方法，共归纳理论探索，提供了几个applicistics发现切割公式CLJ。
2020-08-09 cs.LO cs.PL
Nested Sequents
我们看到如何嵌套序列，超序列的自然概括，使我们能够开发一个系统的模态逻辑证明理论。与其他突出的形式主义，如显示演算和标记序列相反，嵌套序列留在模态语言中，并允许在字面意义上享受子公式属性的证明系统。在第一部分中，我们研究了一套系统的嵌套系统的所有正常模态逻辑形成的一些组合的公理的序列性，自反性，对称性，传递性和欧几里德。我们建立健全性和完整性和他们的一些良好的性质，如可逆的所有规则，结构规则的可接受性，终止证明搜索，以及句法切割消除。在第二部分中，我们研究了常识逻辑，一种具有不动点模态的模态逻辑。我们期待在两个无穷证明系统，这种逻辑：现有的一个普通序列的基础上，没有语法切割消除程序是已知的，和一个新的嵌套序列的基础上。我们看到如何嵌套的序列，在普通的序列相比，允许句法削减消除，从而使我们能够获得一个序数上限的长度证明。
2010-04-11 cs.LO math.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
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
A Cut-free, Sound and Complete Russellian Theory of Definite Descriptions
本文构建了一种带 λ 项与限定摹状词的一阶逻辑矢列演算，在保持罗素式立场的同时将摹状词视为真正项，并给出无切分、构造性切消与 Henkin 式完备性证明。
2024-12-04 cs.LO math.LO
