The Problem of Analogical Inference in Inductive Logic
我们考虑一个问题，这是很大程度上由鲁道夫卡尔纳普在他的工作归纳逻辑，类比推理的问题。在讨论了以前的一些尝试来解决这个问题后，我们提出了一个新的解决方案，该方案是基于Bruno de Finetti关于概率对称性的思想。我们解释我们的新的归纳逻辑可以在归纳逻辑的卡纳皮范式内发展-从一组关于观察过程的简单假设导出归纳规则-并讨论它的一些性质。
2016-06-24 cs.LO
Logic Programming, Functional Programming, and Inductive Definitions
报告了统一逻辑和函数式编程的尝试。作为出发点，我们认为“逻辑程序“不是关于逻辑的，而是构成集合和关系的归纳定义。基于这些考虑的骨架语言设计的草图和原型实现进行了讨论。
2001-03-29 cs.LO
A Logical Study of Some Common Principles of Inductive Definition and its Implications for Knowledge Representation
该定义是人类专家知识的一种常见形式，是形式科学和数学的一个构建块，是数据库理论的基础，并且在许多知识表示和形式规约语言和系统中以各种形式得到支持。本文对科学文本中归纳定义的几种最常见的形式进行了形式化的研究：单调归纳定义、良基序上的归纳定义和迭代归纳定义。我们定义了一个逻辑的定义提供了一个统一的形式语法来表达定义的不同种类，我们定义其语义的忠实形式化的归纳过程。归纳定义的几个基本性质出现了：归纳过程的非决定性，归纳过程的汇合，归纳顺序的作用及其与归纳规则的关系，归纳顺序如何约束归纳过程，最终，归纳顺序是无关紧要的：定义的集合不依赖于归纳顺序。我们提出了一个归纳的建设能够构建的定义集，而不使用归纳顺序。我们调查的那种边界定义，出现在定义悖论。
2017-02-15 cs.LO
A Sequent Calculus for Non-Monotone Inductive Definitions
KU Leuven（荷语鲁汶大学）；Vrije Universiteit Brussel（布鲁塞尔自由大学）
本文提出SCFO(ID)演算，用于处理非单调归纳定义，通过稳定语义验证其理论性质，支持对一般归纳定义的定理形式化证明。
2026-09-23 cs.LO
Entailment Checking in Separation Logic with Inductive Definitions is 2-EXPTIME hard
带有归纳谓词的分离逻辑公式之间的蕴涵，也称为符号堆，已经被证明对于一大类归纳定义是可判定的。最近，提出了一个2-EXPTIME算法，并建立了一个EXPTIME硬界限，但没有精确的下限是已知的。在本文中，我们证明了决定谓词原子之间的蕴涵是2-EXPTIME困难的。证明是基于减少从指数空间有界交替图灵机的成员问题。
2020-04-16 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
A Decision Procedure for Guarded Separation Logic: Complete Entailment Checking for Separation Logic with Inductive Definitions
我们开发了一个双指数决策过程的可满足性问题的保护分离逻辑-一个新的片段的分离逻辑具有用户提供的归纳谓词，布尔连接词，分离连接词，包括限制（保护）版本的否定，魔术棒，和septraction。此外，我们表明，上述任何连接词的警卫下降导致一个不可判定的片段。我们进一步应用我们的决策过程的原因蕴涵在流行的符号堆片段的分离逻辑。特别是，我们获得了一个双指数决策过程之间的蕴涵（无量词）符号堆与有界树宽（SLIDbtw）的归纳谓词定义-分离逻辑的最具表现力的可判定片段之一。再加上最近显示的2 ExpTime-hardness在所述片段中的蕴涵，我们得出结论，SLIDbtw的蕴涵问题是2 ExpTime-complete-从而关闭了以前开放的复杂性差距。
2021-04-20 cs.LO
Extending FO(ID) with Knowledge Producing Definitions: Preliminary Results
Lessius Mechelen（梅赫伦莱修斯大学学院）；KU Leuven（鲁汶大学）
以前的研究ASP和经典逻辑之间的关系已经确定了至少两种不同的方式，前者扩展后者。首先，ASP程序通常包含可以自然地解释为归纳定义的规则集，并且语言FO（ID）已经表明，这样的归纳定义可以以模块化的方式优雅地添加到经典逻辑中。第二，当然还有ASP的著名的认知成分，这主要是在早期关于稳定模型语义的论文中强调的。为了研究这种知识是否也可以以类似的模块化方式添加到经典逻辑中，最近的工作提出了有序认知逻辑的语言。然而，这种逻辑将认知成分与归纳定义成分完全分开，从而忽略了两者之间任何可能的相互作用。在本文中，我们提出了一种语言，扩展的归纳定义结构中发现FO（ID）的认知组件，使这种相互作用成为可能。这项工作的最终目标是发现它是否真的是适当的，以查看的认识组件和归纳定义组件的ASP作为两个独立的扩展经典逻辑，或者是否也有一些重要的东西在两者的结合。
2013-01-08 cs.AI 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
Countability of Inductive Types Formalized in the Object-Logic Level
有限长的整数列表的集合和整数标号的二叉树的集合都是可数无限的。许多归纳定义的类型也有可数的元素。本文给出了Coq语言中一阶归纳定义的形式化语法，并证明了它们在一定条件下是可数的。我们没有用Meta语言编写证明生成器，而是在Coq对象逻辑中开发了一个无公理证明。换句话说，我们的证明是一个依赖类型的Coq函数，从归纳定义的语法到类型的可数性。在此基础上，我们提出了一种Coq策略来自动证明具体归纳类型的可数性。我们还为可数性和归纳定义的语法开发了Coq库，这些库本身就有价值。
2021-07-16 cs.LO
Predicate Logic with Definitions
定义谓词逻辑（英语：Predicate Logic with Definitions，PLD或D-logic）是一阶逻辑的一种修改，主要用于数学的实际形式化。D-逻辑的主要句法结构是术语、公式和定义。定义是变量的定义，常数的定义，或复合定义（D逻辑也有缩写定义，称为缩写）。定义可以在术语和公式中使用。这种可能性使得引入新的类似量词的名称成为可能。复合定义允许从现有定义构造新定义。
1999-06-07 cs.AI cs.LO
Trace Logic for Inductive Loop Reasoning
我们提出了跟踪逻辑，一个多排序的一阶逻辑的实例，自动化的部分正确性验证的程序包含循环。跟踪逻辑概括了程序位置的语义，并通过在任意时间点和循环迭代处对属性进行编码来捕获循环语义。我们引导和自动化的归纳循环推理的跟踪逻辑，通过使用通用跟踪引理捕获归纳循环不变。我们的工作是在RAPID框架中实现的，通过扩展和集成RAPID中基于叠加的一阶推理。我们成功地使用RAPID证明了许多程序的正确性，这些程序的功能行为在线性整数运算、数组和归纳数据类型的一阶理论中得到了最好的总结。
2020-08-06 cs.LO cs.SC
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
Inductive Learning of Logical Theories with LLMs: An Expressivity-Graded Analysis
Idiap Research Institute（伊迪亚普研究所）；University of Manchester（曼彻斯特大学）
本研究提出结合形式化推理引擎反馈的分级分析方法，探究大语言模型在逻辑理论归纳任务中的能力边界，发现大模型可匹敌SOTA ILP系统，但长谓词关系链追踪比理论复杂度更具挑战。
2025-01-14 cs.AI cs.CL cs.LO
Temporal Inductive Logic Reasoning over Hypergraphs
Georgia Institute of Technology（佐治亚理工学院）；Cisco（思科公司）
本文提出时序归纳逻辑推理方法TILR，通过多起点随机B游走和路径一致性算法在时序超图上学习逻辑规则，并发布两个新基准数据集，实验证明其推理能力优于多种强基线。
2024-05-05 cs.AI cs.LG cs.LO
Learning Onto-Relational Rules with Inductive Logic Programming
规则补充和扩展了语义Web上的本体。我们将这些规则称为本体关系，因为它们结合了基于DL的本体语言和支持逻辑编程和演绎数据库传统内的关系数据模型的知识表示形式。规则编写是一项要求非常高的知识工程任务，可以通过应用机器学习算法来部分自动化。在这一章中，我们将展示归纳逻辑程序设计（ILP），诞生于机器学习和逻辑程序设计的交叉点，并被认为是关系学习的主要方法，可以适应本体关系学习。为了说明，我们提供了一个具体的本体关系学习解决方案的问题，学习基于规则的定义DL概念和角色与ILP的细节。
2012-10-29 cs.AI cs.DB cs.LG
The Treewidth Boundedness Problem for an Inductive Separation Logic of Relations
针对一阶逻辑中树宽有界性问题不可判定的情况，本文研究了关系签名上推广的Separation Logic，提出了该逻辑下树宽有界性问题的求解算法。
2024-05-17 cs.FL cs.LO
A Proof Procedure For Separation Logic With Inductive Definitions and Theory Reasoning
本文提出了一种基于逻辑演算的证明方法，结合归纳定义的谓词表示的有界树宽结构和理论推理，检验分离逻辑公式之间蕴涵的有效性。微积分是可靠的和完备的，在这个意义上，证明树是有效的当且仅当它允许一个（可能是无限的）证明树。我们表明，该过程在以下两种情况下终止：（i）当归纳规则，定义谓词发生在左手边的蕴涵终止，在这种情况下，证明树总是有限的。(ii)当理论是空的，在这种情况下，每个有效的证明树都允许一个有理证明树，其中在证明树中出现的成对不同序列的总数是关于r.t.的双指数。最后的结局。
2022-06-22 cs.LO
"Would life be more interesting if I were in AI?" Answering Counterfactuals based on Probabilistic Inductive Logic Programming
Ludwig-Maximilians-Universität München（慕尼黑大学）
本文针对概率逻辑程序在反事实推理中的不足，提出一种语言片段，可从诱导分布重构程序，从而学习支持反事实查询的模型。
2023-08-30 cs.AI cs.LG 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
Enhancing Inductive Entailment Proofs in Separation Logic with Lemma Synthesis
提出了一种基于分离逻辑的引理综合方法，以支持高级归纳蕴涵过程。我们首先提出了一个引理自动证明和系统应用的机制。引理可以包括通用保护和/或未知谓词。虽然前者对于表达性至关重要，但后者对于支持多个谓词之间的关系至关重要。我们进一步引入引理合成来支持（i）自动归纳推理与框架推理以及（ii）定理探索。对于（i）我们在归纳证明过程中自动发现并证明辅助引理;对于（ii）我们自动生成一组有用的引理来关联用户定义或系统生成的谓词。我们已经实现了我们提出的方法到现有的验证系统，并测试其在归纳推理和定理探索的能力。实验结果表明，增强的系统可以自动合成有用的引理，以促进推理的广泛的非平凡归纳证明。
2018-05-12 cs.LO cs.PL
Inductive Logic Programming in Databases: from Datalog to DL+log
Università degli Studi di Bari（巴里大学）
在本文中，我们解决了一个问题，已经引起了数据库社区的注意，随着语义Web的出现，即本体论（和它们所传达的语义）如何帮助解决典型的数据库问题的问题，通过更好地了解KR方面相关的数据库。特别是，我们调查这个问题，从ILP的角度考虑两个数据库的问题，（i）的定义的意见和（ii）的定义的约束，为数据库的模式表示也通过本体。两者都可以重新表述为ILP问题，并可以受益于KR框架DL+log的表达和演绎能力。我们通过实例说明了应用场景。关键词：归纳逻辑程序设计，关系数据库，本体，描述逻辑，混合知识表示和推理系统。逻辑程序设计理论与实践（Theory and Practice of Logic Programming，TPLP）
2010-03-12 cs.AI cs.DB cs.LG
The failure of cut-elimination in cyclic proof for first-order logic with inductive definitions
本文证明带归纳定义的一阶逻辑循环证明系统中切割消除不成立，通过构造一个必须依赖切割规则才能证明的相继式实例，证实了该系统无法消除切割的猜想。
2024-02-15 cs.LO math.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
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
Lifting Symmetry Breaking Constraints with Inductive Logic Programming
University of Klagenfurt（克拉根福大学）；Graz University of Technology（格拉茨工业大学）
有效地省略对称的解决方案的候选人是必不可少的组合问题的解决。大多数现有的方法是特定于实例的，并专注于自动计算对称破缺约束（SBC）为每个给定的问题实例。然而，这种方法应用于大规模的实例或高级问题编码可能是有问题的，因为计算的SBC是命题的，因此，既不能被有意义地解释，也不能被转移到其他实例。因此，在每次调用求解器之前，必须对SBC进行耗时的重新计算。为了克服这些限制，我们引入了一个新的面向模型的方法，答案集编程，升降机的小问题实例的SBC到一组可解释的一阶约束，使用归纳逻辑程序设计范式。实验表明，我们的框架学习的能力，从实例特定的SBC的组合问题的集合的一般约束。所得到的结果表明，我们的方法显着优于一个国家的最先进的具体实例的方法，以及直接应用的求解器。
2021-12-23 cs.AI cs.LG 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
From Circuit Evidence to Mechanistic Theory: An Inductive Logic Approach
Department of Computer Science, University of Manchester（曼彻斯特大学计算机科学系）；Idiap Research Institute（Idiap研究机构）；CRUK National Biomarker Centre, University of Manchester（曼彻斯特大学癌症研究联盟国家生物标志物中心）
本文提出了一种基于归纳逻辑的方法，通过将电路解释视为归纳理论构建，为累积的机制科学提供形式化基础设施。该方法通过因果功能签名和建筑签名，明确机制主张，并在不同模型规模之间实现可移植性。
2026-05-20 cs.AI cs.LG cs.LO
ANDRE: An Attention-based Neuro-symbolic Differentiable Rule Extractor for Inductive Logic Programming
Dept. of Mechanical and Aerospace Engineering, George Washington University, USA（机械与航空航天工程系，乔治华盛顿大学）；Dept. of Mechanical Engineering Sciences, University of Surrey, UK（机械工程科学系，萨里大学）
提出ANDRE框架，通过注意力驱动的可微逻辑算子优化连续规则空间，实现从概率数据中学习一阶逻辑规则，在噪声环境下保持鲁棒性和可解释性。
2026-05-31 cs.AI cs.LG 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
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
GLIDR: Graph-Like Inductive Logic Programming with Differentiable Reasoning
Georgia Institute of Technology（佐治亚理工学院）
提出GLIDR可微规则学习方法，通过可微消息传递算法支持分支和循环等复杂逻辑规则结构，在知识图谱补全任务上显著优于现有方法且能与神经网络端到端联合优化。
2025-08-08 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
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
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
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
Towards One-Shot Learning for Text Classification using Inductive Logic Programming
University of Surrey（萨里大学）
本文提出利用归纳逻辑编程中的元解释学习框架，结合ConceptNet常识知识，实现从极少量样本进行文本分类的一次性学习，并发现示例复杂度越高准确率越高。
2023-08-30 cs.CL cs.LG cs.LO
Best-Effort Inductive Logic Programming via Fine-grained Cost-based Hypothesis Generation
Technische Universität Wien（维也纳技术大学）；Marmara University（马尔马拉大学）；Karlsruhe Institute of Technology（卡尔斯鲁厄理工学院）；Sabanci University（萨班哲大学）
本文介绍了参加第一届归纳逻辑程序设计（ILP）竞赛的计算机系统。它基于Answer Set Programming（ASP）。假设空间生成的ASP编码：给定一组表示模式偏差的事实和一组成本配置参数，该编码的每个答案集表示一个规则，该规则被认为是用于找到需要给定示例的假设。与使用规则体的长度作为规则复杂性度量的最新方法相比，我们的方法允许对假设候选规则的形状进行更细粒度的规范。系统迭代地增加规则成本限制，从而增加搜索空间，直到找到合适的假设。该系统搜索一个假设，需要一个单一的例子，利用ASP编码从XHAIL中使用的编码派生。我们用ILP竞赛的开发和测试集进行实验。为了比较，我们还适应了ILASP系统处理竞争的情况下。实验结果表明，假设搜索空间的代价参数是在有限的资源范围内找到竞争实例的假设的重要因素。
2018-02-23 cs.AI cs.LG cs.LO
Cut Elimination for a Logic with Induction and Co-induction
证明搜索已被用于指定广泛的计算系统。为了建立一个框架，这样的规范推理，我们使用了一个微积分，涉及感应和共感应。这些证明原则是基于定义的证明理论（而不是集合论）概念。定义类似于逻辑程序，其中定义原子的左规则和右规则允许人们将理论视为“封闭的”或定义不动点。定义和自由相等的使用使得有意识地推理语法成为可能。我们以一致的方式添加规则前和后固定点，从而允许用户的原因归纳和共归纳的计算系统的属性，充分利用高阶抽象语法。一致性是保证通过削减消除，在那里，我们给第一，据我们所知，削减消除程序存在的一般归纳和共归纳的定义。
2010-09-30 cs.LO
