Countability of Inductive Types Formalized in the Object-Logic Level
有限长的整数列表的集合和整数标号的二叉树的集合都是可数无限的。许多归纳定义的类型也有可数的元素。本文给出了Coq语言中一阶归纳定义的形式化语法，并证明了它们在一定条件下是可数的。我们没有用Meta语言编写证明生成器，而是在Coq对象逻辑中开发了一个无公理证明。换句话说，我们的证明是一个依赖类型的Coq函数，从归纳定义的语法到类型的可数性。在此基础上，我们提出了一种Coq策略来自动证明具体归纳类型的可数性。我们还为可数性和归纳定义的语法开发了Coq库，这些库本身就有价值。
2021-07-16 cs.LO
Infinitary and Cyclic Proof Systems for Transitive Closure Logic
传递闭包逻辑是通过引入传递闭包算子而获得的一阶逻辑的已知扩展。虽然其他具有归纳定义的一阶逻辑的扩展是由一组归纳定义先验参数化的，但传递闭包算子的添加一致地捕获了所有有限归纳定义。在本文中，我们提出了一个无穷证明系统的传递闭包逻辑，这是一个无限下降式对应的现有（显式归纳）证明系统的逻辑。我们表明，作为一阶逻辑与归纳定义的类似系统，我们的无穷系统是完整的标准语义和包含显式系统。此外，传递闭包算子的一致性允许使用简单的语法标准来定义语义上有意义的完整限制。因此，对规则无穷（即循环）证明的限制为自动化归纳推理的有效系统提供了基础。
2018-06-28 cs.LO
Separation Logic with Linearly Compositional Inductive Predicates and Set Data Constraints
我们确定差异约束集约束（DBS），一个类比的差异约束算术约束集。DBS不仅可以表示集合约束，而且可以表示集合元素上的算术约束。我们将DBS集成到具有线性组合归纳谓词的分离逻辑中，获得其中可以指定线性数据结构的集合数据约束的逻辑。我们证明了这个逻辑的可满足性是可判定的。决策过程的一个关键步骤是计算DBS可定义的集合关系的传递闭包，为了捕获它，我们提出了一种扩展的量化集合约束与Presburger算术（RQSPA）。RQSPA的可满足性，然后证明是可判定的利用先进的自动机理论技术。
2018-11-02 cs.LO
Positive Inductive-Recursive Definitions
提出了一种新的数据类型理论，它允许将类型定义为某些函子Fam（C）-> Fam（C）的初始代数.这个理论，我们称之为积极的归纳递归定义，是一个概括的Dybjer和Setzer的理论归纳递归定义内的C必须是离散的-我们的工作因此可以被视为解除这一限制。这是一个实质性的努力，因为我们不仅需要为这样的数据类型引入一种类型的代码（如Dybjer和Setzer的工作），而且还需要在这样的代码之间引入一种类型的态射（这在Dybjer和Setzer的开发中是不需要的）。我们展示了这些代码如何被解释为Fam（C）上的函子，以及这些代码的态射如何被解释为这些函子之间的自然变换。然后，我们给出了一个应用程序的积极的归纳递归定义的理论嵌套数据类型，我们给出了具体的例子，递归函数定义在宇宙中使用其消除原则。最后，我们证明存在的积极的归纳递归定义适应Dybjer和Setzer的集理论模型，我们的设置。
2015-03-26 cs.LO
An Inductive Construction for Many-Valued Coalgebraic Modal Logic
在本文中，我们提出了一个抽象的框架，多值模态逻辑的原子命题和模态算子的解释为谓词提升余代数上的一个endofunctor的集合范畴。它将Pattinson的共形模态逻辑分层方法推广到多值情形。与规范模型构造和过滤的标准技术相比，该方法采用归纳原理来证明逻辑的可靠性、完备性和有限模型性质。因此，我们可以解除对先前方法的限制~ \cite{Lin2022}，该方法要求底层语言必须具有内在化元级真值赋值操作的表达能力。
2022-10-24 cs.LO
Deciding Separation Logic with Pointer Arithmetic and Inductive Definitions
本文研究允许归纳定义内含指针算术的分离逻辑片段 SLAH，通过归纳定义摘要的线性化及空间原子匹配切分，给出可满足性与蕴含判定过程，并在内存分配器验证任务上验证性能。
2024-03-04 cs.LO
Deciding Entailments in Inductive Separation Logic with Tree Automata
具有归纳定义的分离逻辑（SL）是用于指定复杂递归数据结构的自然形式主义，用于操作此类结构的程序的组合验证。任何基于SL的自动验证过程的关键要素是蕴涵问题的可判定性。在这项工作中，我们减少了蕴涵问题的一个非平凡的子集SL描述树（和超越）的语言包含树自动机（TA）。我们的减少提供了严格的复杂性界限的问题，并表明在我们的片段的蕴涵是EXPTIME完成。出于实用的目的，我们利用自动机理论的最新进展，如包含检查非确定性TA避免明确的确定性。我们实现了我们的方法，并提出了有前途的初步实验结果。
2014-02-11 cs.LO
Tractable and Intractable Entailment Problems in Separation Logic with Inductively Defined Predicates
本文研究分离逻辑中带归纳定义谓词的蕴涵问题，针对P规则和loc-deterministic归纳规则片段给出多项式时间的可靠完备循环证明过程，并证明条件放宽后问题不可处理。
2025-07-11 cs.LO
Extending Classical Logic with Inductive Definitions
本文的目的是扩展经典逻辑与归纳定义的广义概念支持积极和消极的归纳，探讨这种逻辑的性质，它与其他逻辑领域的非单调推理，逻辑程序设计和演绎数据库的关系，并显示其应用的知识表示通过给出一个类型的定义知识。
2000-03-07 cs.AI cs.LO
Classical System of Martin-Lof's Inductive Definitions is not Equivalent to Cyclic Proofs
本文证明循环证明系统CLKID-omega与Martin-Löf归纳定义经典逻辑LKID不等价，通过构造Henkin模型展示2-Hydra命题在CLKID-omega可证而在LKID不可证。
2019-07-31 cs.LO
Trace Logic for Inductive Loop Reasoning
我们提出了跟踪逻辑，一个多排序的一阶逻辑的实例，自动化的部分正确性验证的程序包含循环。跟踪逻辑概括了程序位置的语义，并通过在任意时间点和循环迭代处对属性进行编码来捕获循环语义。我们引导和自动化的归纳循环推理的跟踪逻辑，通过使用通用跟踪引理捕获归纳循环不变。我们的工作是在RAPID框架中实现的，通过扩展和集成RAPID中基于叠加的一阶推理。我们成功地使用RAPID证明了许多程序的正确性，这些程序的功能行为在线性整数运算、数组和归纳数据类型的一阶理论中得到了最好的总结。
2020-08-06 cs.LO cs.SC
A New Algorithm to Automate Inductive Learning of Default Theories
在广义概念的归纳学习中，算法应该能够将概念示例与异常和噪声数据区分开。通过递归发现异常中的模式的方法对应于学习默认理论的问题。默认逻辑是人类在常识推理中使用的逻辑。因此，人类更好地理解了习得默认理论。在本文中，我们提出了新的算法来学习非单调逻辑程序形式的默认理论。实验结果表明，该算法比传统的基于归纳逻辑程序设计的方法有了显著的改进。
2017-07-10 cs.LO
Complete Cyclic Proof Systems for Inductive Entailments
当归纳定义中的基约束分别属于（i）具有规范Herbrand解释的一阶逻辑和（ii）分离逻辑的无量词片段时，本文给出了互递归谓词模型的最小集之间包含问题的循环证明系统.受经典的自动机理论技术的启发，证明树自动机之间的语言包含，我们给出了一个小的推理规则集，被证明是健全的和完整的，在一定的语义限制下，涉及的一组约束条件的归纳系统。此外，我们调查的可判定性和计算复杂性，这些限制的所有考虑的逻辑片段，并提供了一个证明搜索半算法，成为一个决策过程的蕴涵问题，对于那些系统，满足的限制。
2018-04-30 cs.LO
Expressiveness Results for an Inductive Logic of Separated Relations
本文比较关系分离逻辑SLR与（一元）二阶逻辑的表达力，证明二者在无界树宽结构上不可比较，并给出SLR可嵌入SO及MSO在特定有界树宽条件下成为SLR严格子集的结果。
2023-07-05 cs.LO
Quotient inductive-inductive types
同伦类型论（HoTT）中的高阶归纳类型（HIT）允许定义具有定义类型上的等式的构造函数的数据集。HIT概括了商类型，并允许定义在HoTT意义上不是集合的类型（即不满足等式证明的唯一性），例如球体，悬浮体和环面。然而，HIT也有一些有趣的用法来定义集合，比如柯西实数、多项式和类型论的内部、总体语法。在每个例子中，我们定义了几个相互依赖的类型，即它们是归纳-归纳定义。我们称这些HIT为商归纳-归纳类型（QIIT）。虽然最近在HIT的一般理论方面取得了一些进展，但等式构造子和归纳-归纳的结合尽管有许多有趣的应用，但还没有理论基础。在本文中，我们提出了第一步的语义定义QIIT。特别是，我们给出了一个初始代数语义，并表明这是等价的部分归纳原则，这证明了直观预期的消除规则。
2017-11-16 cs.LO
LPC(ID): A Sequent Calculus Proof System for Propositional Logic Extended with Inductive Definitions
Carnegie Mellon University（卡内基梅隆大学）；Katholieke Universiteit Leuven（鲁汶大学）
逻辑FO（ID）使用来自逻辑编程领域的思想来扩展具有非单调归纳定义的一阶逻辑。这种逻辑形式上扩展了逻辑程序设计、溯因逻辑程序设计和数据逻辑，从而将对这些形式主义的看法形式化为（广义）归纳定义的逻辑。本文的目标是研究FO（ID）的命题片段PC（ID）的演绎推理方法。我们引入了一个正式的证明系统的基础上的演算（根森式演绎系统），这种逻辑。由于PC（ID）是经典命题逻辑和命题归纳定义的集成，我们的推理演算证明系统集成了命题演算和定义的推理规则。我们提出了这个证明系统的可靠性和完整性，相对于PC（ID）的一个略有限制的片段。我们还提供了PC（ID）的一些复杂性结果。通过对PC（ID）证明系统的开发，有助于加深对FO（ID）证明理论基础的理解，从而研究FO（ID）的有效证明系统。
2012-07-11 cs.AI cs.LO
The Logic of Logic Programming
本文主张逻辑编程的本质是归纳定义逻辑而非经典逻辑的 Horn 子句子逻辑，并以此解释 Prolog 程序与数学归纳定义的根本相似性，为相关语义问题提供自然解答。
2023-04-26 cs.LO
Cyclic proof theory of generalised inductive definitions
University of Gothenburg（哥德堡大学）；University of Birmingham（伯明翰大学）
本文研究μPA的循环证明系统，证明循环μPA与归纳μPA证明论强度相同，还证明μPA的带注释与普通循环证明可证相同定理，推进了算术理论的非良基证明论分析。
2026-07-30 cs.LO
The Treewidth Boundedness Problem for an Inductive Separation Logic of Relations
针对一阶逻辑中树宽有界性问题不可判定的情况，本文研究了关系签名上推广的Separation Logic，提出了该逻辑下树宽有界性问题的求解算法。
2024-05-17 cs.FL cs.LO
Unifying Decidable Entailments in Separation Logic with Inductive Definitions
分离逻辑\cite{IshtiaqOHearn01,Reynolds02}中的蕴涵问题$φ\models ψ$，在分离的等式（$x \iseq y$和$x \not\iseq y$）、空间（$x \mapsto (y_1,\ldots,y_\rank)$）和谓词（$p(x_1,\ldots,x_n)$）原子的合取之间，由有限的归纳规则集解释，一般是不可判定的.对归纳定义集的某些限制导致可判定类的蕴涵问题。目前，基于两个限制，存在两个这样的可判定类，分别称为\emph{establishment} \cite{IosifRogalewiczSimacek13,KatelaanMathejaZuleger19,PZ20}和\emph{restrictedness} \cite{EIP21a}。通过分别从\cite{PZ20}和\cite{EIP21a}得到的独立证明，证明了这两类问题都是\twoexptime \，并给出了\cite{EIP21a}的多-一约化.在本文中，我们严格推广的限制类，通过区分的条件，仅适用于左（$φ$）和右（$ψ$）的左手边的蕴涵，分别。我们提供了一个多-一减少这个广义类，称为\emph{safe}，建立类。再加上减少建立限制蕴涵问题，这个新的减少关闭循环，并表明三类蕴涵问题（分别建立，限制和安全）形成一个单一的，统一的，\twoexptime -完整的类。
2021-02-15 cs.LO
(Co)inductive Proof Systems for Compositional Proofs in Reachability Logic
可达性逻辑是一种形式主义，可用于表达迁移系统的部分正确性。在本文中，我们提出了三个证明系统的形式主义，所有这些都是健全的和完整的，并继承了共归纳逻辑的性质。然而，证明系统在几个方面有所不同。首先，他们使用归纳和共归纳的比例不同。第二个方面是组合性，广义上意味着它们能够在较小的系统上证明更简单的公式，并将这些公式作为引理重用于较大的系统上的更复杂的公式。第三方面是它们的合理性证明的困难。我们发现，更多的归纳证明系统的使用，更专业的是它的使用coinduction（相对于我们的问题域），更组成的证明系统，但更困难的合理性证明变得。我们还简要地介绍了这些结果在Isabelle/HOL和Coq证明助手的机制。
2019-09-04 cs.LO
Enhancing Inductive Entailment Proofs in Separation Logic with Lemma Synthesis
提出了一种基于分离逻辑的引理综合方法，以支持高级归纳蕴涵过程。我们首先提出了一个引理自动证明和系统应用的机制。引理可以包括通用保护和/或未知谓词。虽然前者对于表达性至关重要，但后者对于支持多个谓词之间的关系至关重要。我们进一步引入引理合成来支持（i）自动归纳推理与框架推理以及（ii）定理探索。对于（i）我们在归纳证明过程中自动发现并证明辅助引理;对于（ii）我们自动生成一组有用的引理来关联用户定义或系统生成的谓词。我们已经实现了我们提出的方法到现有的验证系统，并测试其在归纳推理和定理探索的能力。实验结果表明，增强的系统可以自动合成有用的引理，以促进推理的广泛的非平凡归纳证明。
2018-05-12 cs.LO cs.PL
Inductive Logic Programming via Differentiable Deep Neural Logic Networks
Georgia Institute of Technology（佐治亚理工学院）
提出了一种新的范式，通过深度递归神经网络解决归纳逻辑程序设计（ILP）问题。这个建议的ILP求解器的设计基础上，通过正向链接的演绎微分实现。与以往的大多数方法不同，本文通过引入一种新的可微神经逻辑（dNL）网络，直接学习符号逻辑谓词规则，而不是使用一些限制性规则模板搜索可能的一阶逻辑规则空间。所提出的dNL网络能够以显式的方式有效地学习和表示布尔函数。我们表明，建议的dNL-ILP求解器支持理想的功能，如递归和谓词发明。此外，我们研究了所提出的ILP求解器在涉及基准关系数据集的分类任务中的性能。特别是，我们表明，我们提出的方法在Mutagenesis，Cora和IMDB数据集的分类任务中优于最先进的ILP求解器。
2019-06-08 cs.AI cs.LO
Cut Elimination for a Logic with Induction and Co-induction
证明搜索已被用于指定广泛的计算系统。为了建立一个框架，这样的规范推理，我们使用了一个微积分，涉及感应和共感应。这些证明原则是基于定义的证明理论（而不是集合论）概念。定义类似于逻辑程序，其中定义原子的左规则和右规则允许人们将理论视为“封闭的”或定义不动点。定义和自由相等的使用使得有意识地推理语法成为可能。我们以一致的方式添加规则前和后固定点，从而允许用户的原因归纳和共归纳的计算系统的属性，充分利用高阶抽象语法。一致性是保证通过削减消除，在那里，我们给第一，据我们所知，削减消除程序存在的一般归纳和共归纳的定义。
2010-09-30 cs.LO
The failure of cut-elimination in cyclic proof for first-order logic with inductive definitions
本文证明带归纳定义的一阶逻辑循环证明系统中切割消除不成立，通过构造一个必须依赖切割规则才能证明的相继式实例，证实了该系统无法消除切割的猜想。
2024-02-15 cs.LO math.LO
A Logic for Non-Monotone Inductive Definitions
著名的归纳法原理包括单调归纳法和各种非单调归纳法，如膨胀归纳法、良基集上的归纳法和迭代归纳法。在这项工作中，我们定义了一个逻辑形式化归纳良好的基础集和单调和迭代归纳。正如正归纳原理已在FO（LFP）中形式化，膨胀归纳原理已在FO（IFP）中形式化一样，本文在一种新的非单调归纳定义逻辑（ID-逻辑）中形式化了迭代归纳原理。逻辑的语义受到逻辑编程的良基语义的强烈影响。我们的主要结果是关于ID逻辑中归纳定义的模性质。具体而言，我们制定的条件下，同时定义$\D$的几个关系是逻辑上等同于一个连接的较小的定义$\D_1 \land ... \land \D_n$与不相交的定义谓词。这个结果的困难来自这样一个事实，即分别在$\D_i$和$\D_j$中定义的谓词$P_i$和$P_j$可以通过同时归纳相互连接。由于良基语义下的逻辑程序设计和溯因逻辑程序设计是我们的逻辑的适当片段，我们的模块性结果也适用于那里。
2005-01-13 cs.AI cs.LO
A Query-Driven Decision Procedure for Distributed Autoepistemic Logic with Inductive Definitions
具有归纳定义的分布式自认知逻辑（dAEL（ID））是最近提出的一种用于基于SAYS的访问控制的非单调逻辑。我们定义了一个查询驱动的决策过程dAEL（ID），在知识库系统IDP中实现。决策过程的设计方式，它允许一个确定访问权，同时避免冗余的信息流之间的主体，以提高安全性和减少隐私的关注。考虑到决策过程在最坏情况下具有指数运行时间，它将被视为增加我们对dAEL（ID）的理解的概念证明，而不是被部署用于访问控制系统。
2019-10-09 cs.CR cs.LO
Truth Predicate of Inductive Definitions and Logical Complexity of Infinite-Descent Proofs
Nagasaki University（长崎大学）；National Institute of Informatics / Sokendai（信息学国立研究所/综合研究大学院大学）
本文研究了无限下降证明系统LKID-omega中可证性的逻辑复杂性，证明其为(Pi-1-1)-完全。
2026-03-04 cs.CC cs.LO
Equivalence of Intuitionistic Inductive Definitions and Intuitionistic Cyclic Proofs under Arithmetic
循环证明系统为我们提供了另一种表示归纳定义和有效证明搜索的方法。2011年，Brotherston和Simpson证明了经典循环证明系统的可证明性与马丁-洛夫归纳定义的经典系统的可证明性之间的等价性。本文研究直觉逻辑中的猜想。本文首先指出，FOSSACS 2017年论文的反模型表明直觉逻辑的猜想一般是错误的。然后证明了直觉逻辑的猜想在算术下成立，即直觉循环证明系统与Martin-Lof归纳定义的直觉系统在都包含Heyting算术HA时的可证性相同。为此，本文还证明了HA证明了归纳法的Podelski-Rybalchenko定理和归纳法的Kleene-Brouwer定理。这些结果立即为同一作者在LICS 2017论文中提出的经典逻辑算术下的猜想提供了另一个证明。
2017-12-10 cs.LO math.LO
Constructing Infinitary Quotient-Inductive Types
本文介绍了一个表达类的服从-归纳类型，称为QW-类型。我们表明，在依赖的类型论与唯一性的身份证明，即使是无限的情况下，量子阱类型可以编码使用的组合，涉及严格的正发生的霍夫曼式商类型，和阿贝尔的大小类型的归纳-归纳定义。后者，这提供了一个方便的建设性的抽象什么经典将完成超限序数，被用来证明终止的递归定义的消除和计算性质，我们的编码的量子阱类型。使用Agda定理证明器对开发进行了形式化。
2020-02-19 cs.LO
Layered Fixed Point Logic
我们提出了一个逻辑规范的静态分析的问题，超越了传统上使用的逻辑。它最突出的特点是直接支持行为的归纳计算以及属性的共归纳规范。两个主要的理论贡献是摩尔家族的结果和参数化的最坏情况下的时间复杂度的结果。我们表明，逻辑和相关的求解器可用于快速原型，并说明了各种各样的应用程序内的静态分析，约束满足问题和模型检验。在所有情况下，复杂度结果专门针对经典方法的最坏情况时间复杂度。
2012-04-12 cs.LO
Greatest HITs: Higher inductive types in coinductive definitions via induction under clocks
守护递归是一种强大的模式递归方法，可以看作是步进索引的抽象形式。它目前被广泛用于分离逻辑，通过求解具有负出现的域方程来模拟具有高级功能的程序设计语言。在其多时钟版本中，保护递归也可以用于对共归纳类型进行编程和推理，编码类型中递归定义所需的生产力条件。本文提出了第一种类型论，它结合了多时钟保护递归和立方类型论的特点，并给出了一个指称语义。结合使用高阶归纳类型（Higher Inductive Types，HIT）和保护递归，可以对传统上难以在类型论中表示的共归纳类型进行简单的编程和推理，例如标记转移系统的分支分支类型。例如，我们的研究结果意味着这些双相似性意味着路径平等，因此证明可以沿着双相似性证明。我们的技术贡献之一是一个新的原则下的时钟感应。这允许在时钟上的通用量化与HIT交换直到等价的类型，并且对于共归纳类型的编码至关重要。这种交换性的要求已经制定了归纳类型的公理在以前的类型论与多时钟保护递归，但我们目前的配方作为一个归纳原则允许制定一般的计算规则。
2022-06-03 cs.LO
Constraint Propagation for First-Order Logic and Inductive Definitions
Katholieke Universiteit Leuven（鲁汶大学）
约束传播是许多基于逻辑推理系统的基本推理形式之一。在本文中，我们研究约束传播的一阶逻辑（FO），一个合适的语言来表达各种各样的约束。我们提出了一个算法的约束传播的FO理论和有限结构的背景下，多项式时间的数据复杂度。我们表明，以这种方式的约束传播可以由一个数据库程序表示，该算法可以象征性地执行，即，独立于结构。接下来，我们将该算法扩展到FO（ID），即具有归纳定义的FO的扩展。最后，我们讨论了几个应用程序。
2011-07-08 cs.AI cs.LO
On Automated Lemma Generation for Separation Logic with Inductive Definitions
具有归纳定义的分离逻辑是用于操纵动态数据结构的程序的演绎验证的公知方法。在此上下文中决定验证条件通常基于用户提供的与归纳定义相关的引理。我们提出了一种新的方法自动生成这些引理，这是基于简单的语法标准和确定性的策略，应用它们。我们的方法侧重于迭代程序，虽然它也可以应用于递归程序，以及规范，不仅描述了数据结构的形状，而且还它们的内容或大小。从经验上讲，我们发现我们的方法足够强大，可以处理复杂的基准，例如，搜索，插入，或删除排序列表，二叉搜索树，红黑树和AVL树中的元素的迭代过程，以非常有效的方式。
2015-07-20 cs.LO cs.SE
Model-Guided Synthesis of Inductive Lemmas for FOL with Least Fixpoints
递归定义的链接数据结构嵌入在一个基于指针的堆和他们的性质自然地表示在纯一阶逻辑与最少不动点定义（FO+lfp）与背景理论。这样的逻辑，不像纯粹的一阶逻辑，甚至不承认完整的程序。在本文中，我们采取了一种新的方法来综合归纳假设，以证明在这种逻辑的有效性。我们的想法是利用几种有限的一阶模型作为反例，捕捉公式的不可证明性和无效性，以指导归纳假设的搜索。我们实现我们的程序，并广泛地评估它们涉及堆数据结构的定理，需要归纳证明，并证明我们的方法的有效性。
2022-09-26 cs.LO cs.PL
Decidable Entailments in Separation Logic with Inductive Definitions: Beyond Established Systems
定义了一类分离逻辑公式，其蕴涵问题是：给定公式$ϕ, ψ_1, \ldots, ψ_n$，$ϕ, ψ_1, \ldots, ψ_n$的每个模型是否都是某个$ψ_i$的模型？2 EXPTIME是完整的。该类中的公式是包含谓词原子的存在量化分离合取，由满足一组归纳规则的存储堆结构的最小集合解释，这也是蕴涵问题的输入的一部分。以前的工作考虑建立规则集，这意味着规则中的每个存在量化变量最终必须绑定到分配的位置，即从堆的域。特别是，这保证了每个结构的树宽由集合中最大规则的大小限制。相比之下，在这里，我们表明，建立，虽然足够的可判定性（以及其他两个自然条件），是没有必要的，通过提供一个条件，称为等式限制，这适用于句法（不）平等。在这种情况下，蕴涵问题更加普遍，因为等式限制规则定义了更丰富的结构类，具有无限的树宽。在本文中，我们证明了（1）每一个建立的规则集可以转换成一个等式限制的和（2）蕴涵问题是2 EXPTIME-完全在后一种情况下，从而匹配的复杂性蕴涵为已建立的规则集。
2020-10-11 cs.LO
Differentiable Inductive Logic Programming in High-Dimensional Space
Czech Academy of Sciences Institute of Computer Science（捷克科学院计算机科学研究所）；University of Innsbruck（因斯布鲁克大学）；University of Melbourne（墨尔本大学）
本文扩展 δILP，利用高维梯度下降实现大规模谓词发明，使可微归纳逻辑程序设计能在不预设解结构的情况下解决现有神经符号 ILP 系统无法完成的任务。
2025-01-08 cs.AI cs.LO
Can LLM Aid in Solving Constraints with Inductive Definitions?
本文提出一种神经符号方法，利用大语言模型生成辅助引理，提升求解涉及归纳定义的约束的能力，实验表明其在证明任务上的有效性。
2026-03-12 cs.AI cs.LO
Completeness of Cyclic Proofs for Symbolic Heaps
分离逻辑在理论和实践上都是成功的软件验证方法。符号堆的判定过程是其中的关键问题之一。本文提出了一个具有一般形式归纳定义的符号堆循环证明系统，并证明了它的可靠性和完备性。最后给出了具有归纳定义的符号堆蕴涵的判定过程。具有归纳定义的符号堆的蕴涵的判定性是一个重要的问题。循环证明系统的完备性也是一个重要的问题。本文的结果回答了这两个问题。该判决过程是可行的，因为它是不确定的双指数时间复杂度。
2018-05-28 cs.LO
Inductive and Coinductive Components of Corecursive Functions in Coq
在构造类型论中，递归和上递归的定义受到语法限制，这保证了递归函数的终止性和上递归函数的生产力。然而，许多终止函数和生产函数没有通过语法测试。Bove在她的论文中提出了一个优雅的可访问性谓词方法的重新表述，该方法拓宽了构造类型论中可形式化的终结递归函数的范围。在本文中，我们追求同样的目标生产的上递归函数。值得注意的是，我们的方法的形式化coq生产函数的共归纳定义不仅需要使用特设谓词，而且还需要一个系统的算法，分离归纳和共归纳部分的功能。
2008-07-09 cs.LO
Preprocessing in Inductive Logic Programming
Linacre College University of Oxford（牛津大学李纳克尔学院）
归纳逻辑程序设计是一种机器学习，其中逻辑程序从示例中学习。这种学习通常相对于作为逻辑程序提供的某些背景知识发生。本文介绍了底层预处理，一种在ILP系统必须考虑的程序上生成初始约束的方法。底层预处理将逆蕴涵的思想应用于现代ILP系统。逆蕴涵是Progol引入的一种有影响力的早期ILP方法。本文还提出了$\bot$ -Popper，它是现代ILP系统Popper的底层预处理的一个实现.实验表明，底层预处理可以减少ILP系统在困难问题上的学习时间。当问题中的背景知识量很大时，这种减少可能特别显著。
2021-12-21 cs.AI cs.LG cs.LO
Neuro-Symbolic Inductive Logic Programming with Logical Neural Networks
IBM Research（IBM研究院）
神经符号归纳逻辑程序设计的最新工作已经导致了有前途的方法，可以从嘈杂的，真实世界的数据中学习解释规则。虽然一些建议近似的逻辑运算符与可微运算符从模糊或实值逻辑是无参数的，从而减少了他们的能力，以适应数据，其他方法只是松散的逻辑，使其难以解释学习的“规则”。在本文中，我们提出了学习规则与最近提出的逻辑神经网络（LNN）。与其他神经网络相比，LNN提供了与经典布尔逻辑的强连接，从而允许精确解释学习的规则，同时包含可以使用基于梯度的优化来训练的参数，以有效地拟合数据。我们将LNN扩展到一阶逻辑中的归纳规则。我们对标准基准测试任务的实验证实，LNN规则具有高度的可解释性，并且由于其灵活的参数化，可以达到相当或更高的精度。
2021-12-06 cs.AI cs.LG cs.LO
Effective MSO-Definability for Tree-width Bounded Models of an Inductive Separation Logic of Relations
本文研究关系分离逻辑SLR的MSO可定义性，提出一个可描述有界树宽图集合并能有效翻译为MSO的表达性片段，从而保证可满足性与蕴含问题的可判定性。
2024-02-25 cs.FL cs.LO
Separating the Wheat from the Chaff: Understanding (In-)Completeness of Proof Mechanisms for Separation Logic with Inductive Definitions
Tel Aviv University（特拉维夫大学）；University of Wisconsin-Madison（威斯康星大学麦迪逊分校）
本文研究了分离逻辑中证明机制的不完整性来源，并通过弱分离逻辑的完整性和非标准模型分析，揭示了证明失败的原因。
2025-12-04 cs.LO cs.PL
Induction and Co-induction in Sequent Calculus
证明搜索已被用于指定广泛的计算系统。为了建立一个框架，这样的规范推理，我们使用了一个微积分，涉及感应和共感应。这些证明原则是基于定义的证明理论（而不是集合论）概念。定义类似于（分层的）逻辑程序，其中定义原子的左规则和右规则允许人们将理论视为“封闭的”或定义不动点。定义的使用使得对句法进行内涵推理成为可能，特别是通过统一来强制自由平等。我们以一致的方式添加规则前和后固定点，从而允许用户的原因归纳和共归纳的计算系统的属性，充分利用高阶抽象语法。一致性是保证通过削减消除，在那里，我们给第一，据我们所知，削减消除程序存在的一般归纳和共归纳的定义。
2009-09-30 cs.LO
Combining Fixed-Point Definitions and Game Semantics in Logic Programming
具有定点定义的逻辑程序设计是传统逻辑程序设计的一个有用的扩展。固定点定义可以捕获简单的模型检验问题和封闭世界假设。它的操作语义通常基于直觉可证明性。我们扩展了这些语言的操作语义与游戏语义。这种扩展的语义有几个有趣的方面：特别是，它为$read$谓词提供了逻辑状态。
2015-08-05 cs.LO
Learning Language Representations with Logical Inductive Bias
Tencent AI Lab（腾讯人工智能实验室）
Transformer架构在解决自然语言任务方面取得了巨大的成功，这些任务从大规模未标记的文本中学习强语言表示。在本文中，我们寻求更进一步，探索一个新的逻辑归纳偏见，更好的语言表示学习。逻辑推理是从已知的知识和事实中得出答案的一种形式化方法。受这种观点的启发，我们开发了一种名为FOLNet（一阶逻辑网络）的新型神经架构，以编码这种新的归纳偏差。我们构建了一组神经逻辑运算符作为可学习的Horn子句，这些子句进一步被前向链接到完全可微的神经架构（FOLNet）中。有趣的是，我们发现Transformers中的自我注意模块可以由我们的两个神经逻辑运算符组成，这可能解释了它们强大的推理性能。我们提出的FOLNet具有与其他预训练模型相同的输入和输出接口，因此可以通过使用类似的损失进行预训练/微调。它还允许在替换其他预训练模型时以即插即用的方式使用FOLNet。由于我们的逻辑归纳偏见，通过预训练学习的同一套“逻辑推理技能”预计同样能够解决不同的下游任务。出于这个原因，FOLNet学习具有更强迁移能力的语言表示。几个语言理解任务的实验结果表明，我们的预训练的FOLNet模型优于现有的强转换为基础的方法。
2023-02-19 cs.CL cs.LG cs.LO
Equational and Inductive Reasoning for Maude in Athena
Universidad de los Andes（安第斯大学）；Rensselaer Polytechnic Institute（伦斯勒理工学院）；Pontificia Universidad Javeriana（哈维里亚纳天主教大学）
本文提出maude2athena框架，将Maude的等式理论转换为Athena，支持归纳推理和演绎推理，保持语义并确保简洁性，促进模型检查与定理证明的结合。
2026-04-21 cs.LO
An infinitary model of linear logic
在本文中，我们构造了线性逻辑关系模型的无限变体，其中指数模态被解释为有限或可数多集的集合。我们解释如何解释在这个模型中的不动点算子Y作为一个康威算子交替定义在一个归纳或共归纳的方式。然后，我们扩展的关系语义的颜色或优先级的意义上的奇偶性游戏的概念。这种扩展使我们能够定义一个新的不动点算子Y结合归纳和共归纳的政策。最后，我们勾勒出的结果模型之间的联系，递归和高阶模型检查的演算。
2015-01-28 cs.LO
HyDI: A hybrid Deep Learning-Inductive Logic Programming ensemble for multi-label classification
University of Osnabrück（奥斯纳布吕克大学）
HyDI提出一种结合深度学习与归纳逻辑编程的混合集成架构，用于层次化多标签分类，在ChEBI本体上为314个类别生成规则，提供透明且可解释的分类结果。
2026-09-30 cs.LG cs.LO
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
The Calculus of Algebraic Constructions
本文讨论了代数构造演算（CAC）的基础，CAC是构造演算的归纳数据类型的扩展。CAC通过模式匹配提供函数的定义来概括配备高阶原始递归的归纳类型，该模式匹配捕获满足严格正性条件的任意非依赖和非多态归纳类型的递归定义。CAC还通过提供依赖类型和高阶重写规则来概括抽象数据类型的一阶框架。
2008-05-27 cs.LO
Learning Onto-Relational Rules with Inductive Logic Programming
规则补充和扩展了语义Web上的本体。我们将这些规则称为本体关系，因为它们结合了基于DL的本体语言和支持逻辑编程和演绎数据库传统内的关系数据模型的知识表示形式。规则编写是一项要求非常高的知识工程任务，可以通过应用机器学习算法来部分自动化。在这一章中，我们将展示归纳逻辑程序设计（ILP），诞生于机器学习和逻辑程序设计的交叉点，并被认为是关系学习的主要方法，可以适应本体关系学习。为了说明，我们提供了一个具体的本体关系学习解决方案的问题，学习基于规则的定义DL概念和角色与ILP的细节。
2012-10-29 cs.AI cs.DB cs.LG
Affine functions and series with co-inductive real numbers
我们推广了A. Ciaffaglione和P. Di Gianantonio关于实数精确计算算法的机械验证，使用作为共归纳类型实现的无限数字流。从四个方面进行了研究：第一方面涉及数字流可以与在证明系统中已经公理化（公理化，但没有固定表示）的公理化实数相关的证明。第二个方面重新访问加法函数的定义，寻找让证明搜索机制执行算法的有效构造的技术，该算法通过构造是正确的。第三个方面涉及到一个函数的定义，以计算仿射公式的正有理系数。这应该被理解为一个测试平台，用来描述一种技术，将协递归和递归结合起来，以获得一个算法的模型，该模型乍一看似乎超出了证明系统所允许的表达能力。第四个方面是关于计算级数的函数的定义，以及在计算欧拉数e的级数上的应用。所有这些实验都应该在任何支持共归纳类型，共递归和终止递归的一般形式的证明系统中重现，但我们使用Coq系统进行[12，3，14]。
2006-05-01 cs.LO
