Syntactic Cut-Elimination for Provability Logic GL via Nested Sequents
本文针对可证性逻辑GL切割消去终止性证明困难的问题，提出基于嵌套矢列式的语法化切割消去方法，并借鉴Kushida（2020）的思想，仅用直接归纳避免额外度量和复杂重写，从而消除Poggiolesi（2009）证明中的歧义。
2024-12-31 cs.LO
Combining generic judgments with recursive definitions
程序设计语言的许多语义方面，如它们的操作语义和它们的类型赋值演算，都是通过描述适当的证明系统来指定的。最近的研究已经确定了两个证明理论的功能，允许直接的，基于逻辑的推理这样的描述：原子判断的治疗固定点（递归定义）和编码的约束结构通过通用的判断。然而，包含这两个特征的逻辑迄今为止一直在正交地处理它们：也就是说，它们不提供定义对象逻辑属性的能力，这些属性本身依赖于绑定的内在处理。我们提出了一个新的和简单的集成这些功能的直觉逻辑增强与感应自然数，我们表明，由此产生的逻辑是一致的。集成的关键好处是，它允许递归定义不仅编码简单的，传统形式的原子判断，而且还捕获与这些判断有关的通用属性。这种逻辑的有用性说明了它如何可以提供优雅的处理对象逻辑的情况下，出现在证明涉及类型演算和任意级联的替代，发挥作用，在reductionalarguments。
2008-04-14 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
Nominal Abstraction
递归关系规范通常用于描述形式系统的计算结构。最近的研究证明理论已经确定了两个功能，促进直接的，基于逻辑的推理这样的描述：通过递归定义的原子判断的解释和编码的约束结构通过通用的判断。然而，包含这两个特征的逻辑目前不允许定义体现与绑定相关的动态方面的关系，这是许多推理任务所需的能力。我们提出了一个新的术语之间的关系称为名义抽象作为克服这一缺陷的一种手段。我们将名义抽象到一个丰富的逻辑，也包括定义，通用量化，归纳，并共同归纳，然后我们证明是一致的。我们提出的例子表明，这种逻辑可以提供优雅的治疗绑定的情况下，出现在许多证明，如那些建立属性的类型演算和任意级联替代，在reductionalarguments中发挥作用。
2010-09-23 cs.LO
A Constructive Proof of Cut Elimination for a System of Full Second Order Logic
本文给出了一个完全二阶逻辑系统的割消的构造性证明，它吸收了结构规则，用集合代替序列。通过使用一个新的诱导参数，cutrank增长的标准问题是避免。这种技术也可以应用于一阶逻辑。
2016-06-21 cs.LO math.LO
Integrating a Global Induction Mechanism into a Sequent Calculus
数学中大多数有趣的证明都包含一个归纳论证，这需要扩展LK-演算来形式化。最常用的演算归纳包含一个单独的规则或公理，减少了有效的证明理论性质的演算。据我们所知，没有这样的演算允许割消法成为具有子公式性质的标准形式，即证明中出现的每个公式都是最终公式的子公式。证明图式是LK-证明的变体，能够通过将证明链接在一起来模拟归纳。存在一个模式范式，它与具有子公式性质的范式具有可比的证明理论行为。然而，一个演算的证明图式的建设并不存在。在本文中，我们介绍了一个演算证明图式和证明的可靠性和完整性方面的一个片段的归纳论点形式化的皮亚诺算术。
2017-05-12 cs.LO math.LO
Hybrid: A Definitional Two-Level Approach to Reasoning with Higher-Order Abstract Syntax
众所周知，在逻辑框架中结合高阶抽象语法和（共）归纳是有问题的。以前的工作描述了一个名为混合动力的工具，在伊莎贝尔HOL，其目的是解决许多这些困难的实施。它允许使用高阶抽象语法来表示对象逻辑，并使用策略性定理证明和（共）归纳原理进行推理。在本文中，我们描述了如何使用它在一个多层次的推理方式，类似的精神，其他元逻辑，如BLOMF。通过明确引用证明在一个中间层称为规范逻辑，我们解决了推理的问题（共）归纳存在的非分层假设的判断，这使得非常优雅和简洁的规范对象逻辑推理规则。
2010-05-26 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
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
Quotient inductive-inductive types
同伦类型论（HoTT）中的高阶归纳类型（HIT）允许定义具有定义类型上的等式的构造函数的数据集。HIT概括了商类型，并允许定义在HoTT意义上不是集合的类型（即不满足等式证明的唯一性），例如球体，悬浮体和环面。然而，HIT也有一些有趣的用法来定义集合，比如柯西实数、多项式和类型论的内部、总体语法。在每个例子中，我们定义了几个相互依赖的类型，即它们是归纳-归纳定义。我们称这些HIT为商归纳-归纳类型（QIIT）。虽然最近在HIT的一般理论方面取得了一些进展，但等式构造子和归纳-归纳的结合尽管有许多有趣的应用，但还没有理论基础。在本文中，我们提出了第一步的语义定义QIIT。特别是，我们给出了一个初始代数语义，并表明这是等价的部分归纳原则，这证明了直观预期的消除规则。
2017-11-16 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
CERES for First-Order Schemata
割消法CERES（用于一阶和高阶经典逻辑）是基于特征子句集的概念，它是从LK证明中提取出来的，并且总是不可满足的。这个子句集的归结反驳可以用作仅使用原子割（原子割范式）的证明的框架。这是通过用原始证明的相应投影替换归结反驳中的子句来实现的。我们提出了一个概括的CERES（称为CERES）的一阶证明图式，并定义了一个示意性版本的微积分称为LKS，和原始递归定义的基础上证明模式的概念。提出了一种从这些证明图式中提取图式特征子句集和图式投影的方法。我们还定义了一个用于反驳小句集图式的图式归结演算，它可以用来反驳图式特征小句集。最后将投影图式和分辨图式连接起来，得到了原子割范式的一个图示。CERES的一个主要好处是削减消除归纳定义的证据的延伸：我们比较CERES与标准结石使用归纳规则，并证明CERES是能够执行削减消除传统方法失败。CERES的算法处理得到CERES系统最近扩展的支持。
2013-03-18 cs.LO
Formalisation in Constructive Type Theory of Barendregt's Variable Convention for Generic Structures with Binders
我们引入了一个宇宙的定期datastries变量绑定信息，我们定义了通用的形成和消除（即归纳/递归）运营商。然后，我们定义了一个通用的alpha-等价关系的类型的宇宙的基础上的名称交换，并推导出迭代和归纳的原则，其工作模alpha转换捕捉Barendregt的变量公约。我们实例化所得到的框架，以获得λ演算和系统F，我们推导出替代操作和替代引理的阿尔法转换和替代组合。整个工作是在建构类型论中进行的，并由Agda系统进行机器检查。
2018-07-05 cs.LO cs.PL
A System of Interaction and Structure IV: The Exponentials and Decomposition
我们研究了一个称为NEL的系统，它是用线性逻辑的指数扩充的混合交换/非交换线性逻辑BV。等价地，NEL是用非交换自对偶连接序列扩充的MELL。在本文中，我们展示了NEL的一个基本组合属性，我们称之为分解。这个结果导致了一个割消定理，这将在本系列的下一篇文章中证明。为了控制定理的归纳测度，我们依赖于一种新的技术，该技术从NEL证明中提取指数的结构，我们称之为！流程图
2010-07-27 cs.LO
The Structure of Differential Invariants and Differential Cut Elimination
混合系统验证的最大挑战是微分方程的处理。由于可计算的封闭形式的解决方案只存在于非常简单的微分方程，证明证书已经提出了更可扩展的验证。然而，这些证明证书的搜索过程仍然是相当特殊的，因为对问题结构的理解很差。我们研究微分不变量，它定义了微分方程的归纳原理，并且可以通过使用它们的微分结构来检查微分方程的不变性，而不必求解它们。研究了微分不变量的结构性质。为了分析证明搜索复杂性的权衡，我们确定了几类微分不变量之间的十几种关系，并比较了它们的演绎能力。作为我们的主要结果，我们分析了微分割的演绎能力和带有辅助微分变量的微分不变量的演绎能力。我们反驳了差分切割消除假设，并表明，与标准切割，差分切割的基本证明原则，严格增加了演绎能力。我们还证明了演绎能力进一步增加时，添加辅助微分变量的动态。
2012-11-23 cs.LO math.CA math.DS
A Generalized Resolution Proof Schema and the Pigeonhole Principle
CERES方法是一种对证明模式进行割消的方法，证明模式是一个递归构造的证明序列。证明图式可以被认为是一种规避将归纳规则添加到LK-演算的方法。在这项工作中，我们形式化的无穷鸽子洞原理（IPP）的示意性版本，在LKS演算，并分析提取的子句集模式。然而，我们发现的反驳不能表示为一个归结证明模式，因为没有明确的排序索引递归的条款，每一个排序是在反驳中使用。有趣的是，子句集和它的反驳非常接近于在LK-证明的割消中发现的规范形式。不能处理这种形式的反驳是有问题的，因为证明模式在实例化时是LK证明。基于我们的反驳和结构的结果的结构，我们开发了一个广义的决议证明模式的基础上递归的一种特殊类型的列表，并提供了一个反驳，使用我们的推广，条款集提取我们的形式证明IPP。我们还从反驳中提取了一个Herbrand系统。
2016-08-28 cs.LO
Proof Search Specifications of Bisimulation and Modal Logics for the pi-Calculus
我们指定的操作语义和互模拟关系的有限π演算内的逻辑，其中包含的nabla量词编码通用的判断和定义编码不动点。由于我们只限于有限的情况，逻辑展开不动点的能力使得这个逻辑对于操作语义的归纳性质和互模拟的共归纳性质都是完备的。nabla量词有助于解决π演算表达式中变量范围及其执行（证明）的微妙问题。我们说明了这种逻辑所允许的逻辑规范的几个优点：它们是自然的和说明性的;它们不包含关于变量名的副条件，同时保持对这些变量的完全形式化处理;后期互模拟关系和开放互模拟关系之间的差异来自于熟悉的逻辑区别;三个量词之间的相互作用（对于所有，存在，（nabla）它们的作用域可以解释早期互模拟和晚期互模拟之间的差异以及基于约束输入和输出行为的各种模态算子之间的差异;并且涉及推理规则、统一和回溯的应用的证明搜索可以为模态逻辑中的一步转换、互模拟和满足提供完整的证明系统。我们还说明了如何可以编码的π演算与复制，在一个扩展的逻辑与归纳和共归纳。
2009-02-16 cs.LO
Higher-Order Termination: from Kruskal to Computability
终结性是逻辑学和计算机科学中的一个重要问题。在逻辑中，终止是证明理论的核心，通常被称为强规范化（切割消除）。在计算机科学中，终止性一直是表明程序正确性的一个重要问题。在早期的逻辑中，强规范化通常通过将序数分配给表达式来显示，以这种方式消除切割将产生具有较小序数的表达式。在验证的早期，计算机科学家使用了类似的想法，通过自然数（例如大小）来解释程序调用的参数。显示每个递归调用的参数的大小减少给出了程序的终止证明，然而这是相当弱的，因为它只能产生相当小的序数。在六十年代，泰特发明了一种新的方法来显示自然演绎的切割消除，基于项集合上的谓词，使得表达式对谓词的成员关系暗示了该表达式的强规范化属性。谓词是通过类型上的归纳定义的，或者甚至是作为一个不动点，这种方法可以产生更大的序数。后来Girard以约简或可计算性候选人的名义推广了它，它在证明类型化可达演算的强规范化性质方面表现得非常有效。
2007-01-05 cs.LO
Cut-Simulation and Impredicativity
The University of Cambridge（剑桥大学）；Saarland University（萨尔兰大学）；Jacobs University Bremen（不来梅雅各布大学）
我们研究了非谓词（高阶）逻辑中的割消除和割模拟。我们说明，添加简单的公理，如莱布尼茨方程的演算不可断言的逻辑-在我们的情况下，一个经典的类型论的微积分-就像添加削减。这一现象同样适用于布尔和函数外延性、归纳、选择和描述等重要公理。这就要求微积分的发展，这些原则是内置的，而不是被公理化处理。
2009-03-02 cs.AI cs.LO
A two-level logic approach to reasoning about computations
关系描述已被用于形式化不同的计算概念，包括，例如，操作语义，类型，和接受非确定性机器。因此，我们提出了一个（限制）的逻辑理论的关系作为一种语言来指定这样的概念。我们的规范逻辑的进一步特点是能够显式地处理对象语言中的绑定。一旦这样的逻辑被固定，下一个自然的问题是我们如何证明关于用它写的规范的定理。我们建议使用第二种逻辑，称为推理逻辑，用于此目的。一个令人满意的推理逻辑应该能够完全编码规范逻辑。与规范逻辑相关的是各种绑定概念：公式中的量词，序列中的特征变量，以及术语中的抽象。为了提供这些方面的自然处理，推理逻辑必须编码绑定结构以及它们的范围，自由和绑定变量以及捕获避免替换的相关概念。此外，为了支持有关可证明性的论点，推理逻辑应该拥有通过归纳和协同归纳构建证明的强大机制。我们提供这些功能，在这里使用一个逻辑称为G表示的关系，通过原子判断的定义，包含推理规则的归纳和共归纳，并包括一个特殊的通用量词的条件。我们展示了如何证明在规范逻辑可以透明地编码在G。我们还描述了一个交互式定理证明称为阿贝拉，实现G和这种两级逻辑方法，我们提出了几个例子，证明阿贝拉在推理计算的功效。
2010-09-01 cs.LO cs.PL
Generating Property-Directed Potential Invariants By Backward Analysis
本文讨论了引理生成的问题，在一个k-归纳为基础的形式化分析的过渡系统，在线性实/整数算术片段。向后分析，由量词消去，用于输出原像的否定证明目标，被视为未经授权的状态，或灰色状态。提出了两种方法来利用这一信息来源。首先，彻底探索灰色状态空间的可能分割发现状态变量之间的新关系，代表潜在的不变量。其次，不精确的探索重组和过度近似灰色状态空间的不相交区域，也发现状态变量之间的新关系。k归纳法用于隔离不变量并检查它们是否加强了证明目标。这些算法可以用于向后探索的第一个原像，每次输出一个新的原像，细化灰度状态的信息。在我们的背景下，关键的航空电子嵌入式系统，我们表明，我们的方法是能够优于其他学术或商业工具的例子，在我们的应用领域的兴趣。通过两个主要的例子，其中之一是由罗克韦尔柯林斯公司，在一个合作的形式化验证框架的方法进行了介绍和动机。
2013-01-01 cs.CE cs.LO cs.SE
An Infinitary and a Cyclic Sequent Calculus for Non-Monotone Inductive Definitions
KU Leuven（荷语鲁汶大学）；Vrije Universiteit Brussel（布鲁塞尔自由大学）
本文为 FO(ID) 逻辑中的非单调归纳定义形式化了无限下降原理，通过扩展 LKID{\omega} 和 CLKID{\omega} 得到相继式演算 SCFO(ID)-inf 和 SCFO(ID)-cyc，并证明了可靠性、完备性、消割及与 SCFO(ID) 的关系。
2026-09-23 cs.LO math.LO
Structural focalization
本文提出命题直觉主义逻辑的聚焦矢列演算，借助结构化消切风格的归纳证明其聚焦性、内部可靠性与完备性，主要贡献在于恒等扩张证明。
2014-03-17 cs.LO
Uniform Algebras: Models and constructive Completeness for Full, Simply Typed λProlog
本文为λProlog语言基础逻辑HOHH建立模型论，证明消解的可靠性与完备性，并利用最小不动点及Lindenbaum代数变体给出构造性证明，同时提出新的切割消去方法。
2024-05-23 cs.LO cs.PL math.LO
Towards Weak Stratification for Logics of Definitions
本文探讨了定义逻辑中弱分层条件的兼容性，证明其与通用量化和归纳兼容，并旨在扩展Abella证明助手以支持此类定义。
2026-02-03 cs.LO
Computational Logic for Biomedicine and Neurosciences
在这里，我们主张使用计算逻辑系统生物学，作为一个\emph{unified and safe}框架非常适合于建模的动态行为的生物系统，表达他们的属性，并验证这些属性。潜在的候选逻辑应该有一个传统的证明理论谱系（包括归纳法，或享受割消和聚焦的微积分演示），并应该有经过认证的证明工具。除了提供一个可靠的框架外，这还允许对我们的生物系统进行正确的编码。对于一般的系统生物学，特别是生物医学，我们到目前为止，对于建模部分，有三个候选逻辑：都基于线性逻辑。所研究的性质和它们的证明形式化在一个非常有表现力的（非线性）归纳逻辑：归纳构造演算（CIC）。到目前为止，我们所考虑的例子都是相对简单的例子;然而，所有的例子都在实现CIC的Coq系统中进行了正式的半自动证明。在神经科学中，我们直接使用CIC和Coq来建模神经元和一些简单的神经元回路，并证明它们的一些动力学性质。在生物医学中，多组学途径相互作用的研究，以及临床和电子健康记录数据，将有助于药物发现和疾病诊断。未来的工作包括使用更多的自动校准器。这将使我们能够指定和研究更现实的例子，并在长期提供一个系统的疾病诊断和治疗预后。
2020-10-06 cs.LO q-bio.QM
