https://arxiv.org/pdf/2112.12551

Preprocessing inInductive Logic Programming

归纳逻辑编程中的预处理

归纳逻辑编程（Inductive Logic Programming, ILP）是一种机器学习方法，其中逻辑程序通过从示例中学习得到[22]。这种学习通常相对于以逻辑程序形式提供的某些背景知识进行。本文提出了一种称为“自底向上预处理”（bottom preprocessing）的方法，用于生成ILP系统在考虑逻辑程序时必须满足的初始约束条件。“自底向上预处理”将逆蕴涵（inverse entailment）的思想应用于现代ILP系统。逆蕴涵是早期ILP领域具有影响力的经典方法之一，最初随Progol系统[20]一起提出。本文还介绍了一个名为⊥-Popper的实现，它是为现代ILP系统Popper[7]设计的“自底向上预处理”的具体实现。实验结果表明，“自底向上预处理”可以减少ILP系统在解决复杂问题时的学习时间。当问题中涉及的背景知识量较大时，这种减少尤其显著。

第一章
引言

一个常见的软件工程面试问题要求面试者编写一个程序，该程序能够判断给定的字符序列是否为回文[17]。回文是指从前往后和从后往前读都相同的字符序列[9]。面试官可能会提供一些回文的例子。例如，序列“racecar”、“deed”、“mom”、“a”以及空字符串是正例（positive examples），因为它们是回文。而单词“carriage”、“dead”、“mop”、“at”和“palindrome”则是反例（negative examples）。如果面试者感到困难，可以通过向他们提供一个用于反转字符序列的函数来简化任务。

假设这一任务交给计算机完成。自动生成满足一组规范的程序的问题属于程序合成（program synthesis）领域[10]。本文聚焦于归纳逻辑编程（Inductive Logic Programming, ILP），这是一种可以应用于程序合成的机器学习方法。ILP系统通过示例学习逻辑程序。它们以一组正例、一组反例以及以逻辑程序形式提供的背景知识（Background Knowledge, BK）作为输入。在本文所使用的基于蕴涵学习（learning from entailment）的ILP框架中，一个逻辑程序覆盖某个示例的条件是：该程序在背景知识的支持下逻辑上蕴含该示例。ILP问题的理想解是一个能够覆盖所有正例且不覆盖任何反例的逻辑程序[19, 22]。

ILP系统的优势包括：它们通常可以从非常少的示例中学习[16]，输出的结果是人类可读且可修改的，并且支持迁移学习。对迁移学习的支持意味着一个ILP问题的输出可以用作其他问题的背景知识[29]。这是学习复杂系统时的一个理想特性[6]。

示例1.1（回文识别）
回文识别问题可以使用逻辑编程语言Prolog编码为一个ILP问题。该问题可以用集合(E+, E−, B)表示，其中E+包含正例，E−包含反例，B是背景知识。我们可以将第一段中提到的规范写成如下形式1：

与人类面试者的情况类似，提供一些额外的帮助可以极大地简化问题。

正如示例1.1所示，背景知识的选择对于ILP问题至关重要[4]。理想情况下，提供额外的背景知识可以减少学习时间。然而，许多ILP系统在背景知识规模增加时表现不佳。这种对背景知识规模的敏感性限制了迁移学习在ILP中的实用性[6]。

本文提出了一种名为“自底向上预处理”（bottom preprocessing）的新技术，该技术从ILP问题的示例中计算信息，并利用这些信息来缩小ILP系统需要考虑的程序集合。我展示了自底向上预处理可以减少ILP系统的学习时间。第5章描述的Michalski火车问题实验表明，使用自底向上预处理后，学习时间平均减少了10倍以上。在这些实验的一个变体中，我还展示了当问题的背景知识规模增加时，自底向上预处理也可以显著改善ILP系统的扩展性。

本文还介绍了⊥-Popper，这是将自底向上预处理作为扩展实现到ILP系统Popper[7]中的一个实现。Popper将ILP问题编码为逻辑编程语言Prolog语法上的约束满足问题（CSP）。在ILP中，可能的程序通常被称为假设（hypotheses）。系统探索的所有可能程序的空间被称为假设空间（hypothesis space）。Popper使用“从失败中学习”（learning from failures）技术，在生成失败假设时产生新的约束条件。这些约束条件会从假设空间中剔除假设。Popper的一个局限性是它仅在测试新假设时参考示例。这意味着它的初始假设空间不受问题示例的约束。

早期的ILP系统（如Progol[20]和HAIL[26]）使用了一种称为逆蕴涵（inverse entailment）的技术。与Popper搜索整个程序不同，这些系统一次搜索一条规则以添加到不断增长的假设中。对于每条规则，它们首先从单个正例中计算出一个“自底子句”（bottom clause），然后利用这个自底子句指导搜索最佳规则以添加到假设中。

⊥-Popper的目标是利用早期ILP系统中使用的自底子句来克服Popper初始假设空间的局限性。相对于背景知识B的某示例e的自底子句，记作⊥B(e)，是指逻辑上最具体的能够蕴涵e的子句。通俗地说，⊥B(e)的主体由所有在某些背景知识下e为真时不可能为假的事实组成。任何可以添加到⊥B(e)主体中的其他事实要么无关紧要，要么会否定e。因此，自底子句可以被视为对任何应该出现在假设中的子句设定一个下界。

这一方法立即面临的一个困难是，子句之间的蕴涵关系是不可判定的[2]。因此，自底向上预处理借鉴了逆蕴涵的方法，使用θ-子和（θ-subsumption）来比较子句[25]。θ-子和蕴涵关系成立，但尽管它是可判定的，却比蕴涵关系更弱[24]。正如第3章所示，这种选择的结果是，在某些情况下，⊥-Popper可能会从Popper的假设空间中剔除解。这意味着⊥-Popper在寻找ILP问题的解时是不完备的。第5章的实验表明，这种不完备性在许多ILP问题中并不是一个显著的限制。

⊥-Popper被实现为Popper的一个包装器。它依赖于向Popper提供假设约束作为输入。假设约束是以Popper求解器语言编写的约束，可以用来从假设空间中剔除假设。为了使用从自底子句生成的假设约束，这些约束必须以Popper求解器可用的形式编写。⊥-Popper将约束编码为答案集编程（Answer Set Programming, ASP）语言。它对子句之间的子和检查进行编码，同时还编码了一组针对假设的约束。

Popper属于现代ILP系统的一类，采用元级方法解决ILP问题。元级ILP系统对逻辑程序的结构进行推理。它们通常使用求解器来搜索其假设空间[5]。虽然⊥-Popper的实现特定于Popper，但自底向上预处理可以更广泛地应用于任何支持假设约束的元级ILP系统。

贡献
本文做出了以下贡献：

  1. 它形式化了使用自底向上预处理为元级ILP系统生成假设约束的方法。

  2. 它证明了对ILP问题进行自底向上预处理时：
    (a) 在应用于反例时不会剔除解。
    (b) 在应用于正例时可能会剔除解。然而，存在一个定义明确的解子集，这些解永远不会被这些约束剔除。

  3. 它描述了⊥-Popper，这是为Popper实现自底向上预处理的一个实际应用。

  4. 它通过实验证明了自底向上预处理可以：
    (a) 减少在复杂ILP问题上的学习时间。
    (b) 随着ILP问题中背景知识量的增加，改善元级ILP系统的扩展性。

结构概述
本文的结构如下：

  • 第二章

    确立了自底向上预处理的问题设定。

  • 第三章

    包含与自底向上预处理正确性相关的理论。

  • 第四章

    描述了⊥-Popper的实现。

  • 第五章

    介绍了使用Michalski火车问题[13]和列表操作编程问题的实验结果。

  • 第六章

    讨论了相关工作。

  • 第七章

    总结全文，讨论了自底向上预处理的局限性以及未来可能的研究方向。

第二章
问题设定

本章首先简要概述了逻辑编程，然后精确地定义了自底向上预处理的问题设定。该问题设定是对《通过从失败中学习来学习程序》[7]一文中描述的“从失败中学习”（Learning from Failures, LFF）问题设定的扩展。许多定义仅对原文中的定义进行了轻微修改。

2.1 逻辑编程

假设读者对逻辑编程有一定的了解。以下简要总结旨在明确定义本文中将使用的术语。

2.1.1 语法

2.1.2 语义

逻辑程序的词汇表 V是其所有常量符号、函数符号和谓词符号的集合。Herbrand 宇宙 是由 V中的常量符号和函数符号构造出的所有基项的集合。Herbrand 基 是由 V中的谓词符号和 Herbrand 宇宙中的基项构造出的所有基原子的集合。一个Herbrand 解释 是 Herbrand 基的一个子集。在 Herbrand 解释中的原子被视为真，而不在 Herbrand 解释中但属于 Herbrand 基的原子被视为假[5, 24]。

2.1.3 逻辑编程语言

Datalog 是一种逻辑编程语言，使用上述语法的一个子集。Datalog 程序由确定性子句组成。Datalog 不允许嵌套的复合项。这意味着 Datalog 程序具有有限的 Herbrand 基。Datalog 要求子句头中的每个变量也必须出现在体中。这些限制使得 Datalog 程序是可判定的，因此可以保证终止[5]。

Prolog 是一种流行的、图灵完备的逻辑编程语言。它允许使用语法部分中描述的所有语法。然而，Prolog 并不是一种纯粹的声明式语言[5]。尽管 Prolog 表达能力很强且被广泛使用，但要精确地对其进行推理可能会相当困难。Popper 既能生成 Prolog 程序，也能将 Prolog 程序作为输入。

答案集编程（Answer Set Programming, ASP） 是一种逻辑编程类型，非常适合用于定义和求解约束满足问题。其语法类似于上述逻辑程序的语法，并包含本论文未讨论的扩展功能。Popper 使用 ASP 来编码其约束满足问题（CSP）。

2.2 问题定义 2.2.1 语言偏置

到目前为止，ILP 系统的假设空间仅被松散地定义。在大多数情况下，一个算法可能探索的所有程序的总集合是无限的。在示例 1.1 中，隐含地假设了只有出现在背景知识中的谓词符号才能在假设中使用。然而，大多数 ILP 系统使用语言偏置 作为一种归纳偏置，以精确地定义其假设空间[5]。

2.2.1.1 模式声明

逆蕴涵（inverse entailment）框架[20]首次提出了模式声明，作为建立其语言偏置的一种手段。如今，许多 ILP 系统都使用模式声明[20, 27, 26, 15]。LFF（从失败中学习）问题设定使用了一组不同但同构的声明来定义其语言偏置。这里简要解释模式声明，因为它们对于自底子句的计算非常重要，并且在 ILP 文献中也经常出现。

模式声明的形式为 modeh(r, atom) 或 modeb(r, atom)。其中，modeh 声明限制了假设子句头中原子的形式，而 modeb 声明限制了体中原子的形式。

示例 2.1（模式声明）
示例 1.1 的模式声明可能包括：

2.2.1.2 声明定义

原始 LFF 问题设定的语言偏置不需要召回率、方向或类型。然而，方向和类型对于限制自底子句的计算非常有用。在此，LFF 问题设定的声明被扩展以包括类型和方向声明。

这些定义确立了语言偏置的语法。然而，尚未说明这些声明对假设空间实际施加的限制。第一步是定义一个子句与给定语言偏置一致的含义。

2.2.2 假设约束
自底向上预处理通过为元级 ILP 系统生成一组假设约束来运行。这些约束的具体语言可能因目标 ILP 系统的不同而有所差异。因此，为了保持问题设定的通用性，假设约束被定义为它们如何影响假设空间。⊥-Popper 实现中使用的具体假设语言将在第 4 章中给出。

2.2.3 问题输入

在定义了 LFF 问题的语言偏置和假设约束后，现在可以完整描述一个 LFF 问题的输入。

定义 11（LFF 问题输入）

对背景知识的限制是为了确保以下三点：

  1. 问题不会因为背景知识蕴含某个反例而变得显然不可满足。

  2. 没有正例是无关的，否则背景知识在没有假设的情况下就能蕴含该正例。

  3. 背景知识中的子句不能与假设中的子句进行归结。这确保了由于背景知识中的子句，假设不会变得递归。

2.2.4 解

在定义了 LFF 问题输入之后，现在可以正式定义在 LFF 框架下，一个假设成为问题解的含义。

处理误分类示例（一种噪声）的能力在许多类型的机器学习中非常重要[8]。LFF 问题设定以及延伸的自底向上预处理都假设所有示例都被正确分类。如果示例中存在噪声，LFF 系统可能无法找到解。

许多元级 ILP 系统会在最优解存在时学习该解[5]。定义最优性的方式有很多种。在 LFF 问题设定中，最优性是通过程序大小来定义的。

2.3 泛化与特化

在子句之间决定蕴涵关系是不可判定的[2]。由于这一原因，基于逆蕴涵（inverse entailment）的系统使用一种称为子和（subsumption） 的较弱关系来测试子句之间的蕴涵关系。

第三章

预处理理论

本文的核心思想是利用 ILP 问题中关于示例和背景知识的信息，来修剪其初始假设空间。这可以通过对示例进行预处理以生成一组额外的假设约束来实现。

备注 ：在本章中，假设 LFF 问题输入的背景知识（BK）是一个具有有限 Herbrand 基的确定性程序。

这一假设的结果是，BK 是单调的，并且不允许函数符号（也称为无函数形式）。在第 4 章中，将描述在实践中处理无限 Herbrand 基的方法。

3.1 预处理问题

定义 19（预处理问题）

3.2 自底向上预处理

预处理是任何支持假设约束的元级 ILP 系统的一种可选方法。通过预处理可以生成许多不同的假设约束方法。本论文的其余部分将重点关注从 ILP 问题中示例的自底子句生成的假设约束。这种方法被称为自底向上预处理 ，并在本节末尾正式定义。

3.2.1 自底子句

定义 23（自底子句）

需要注意的是，如果自底子句存在，那么符合偏置一致性的自底子句也总是存在的。在极端情况下，符合偏置一致性的自底子句就是将示例事实提升为变量的形式。第 4 章描述了一种自底子句算法，该算法直接找到一个示例的符合偏置一致性的自底子句。

下一个命题是自底向上预处理方法的核心。它表明，相对于背景知识，一个泛化了某个示例自底子句的假设会蕴涵该示例本身。这是逆蕴涵中的一个众所周知的结果，可以作为原始表述[20]的一个推论。这里重新推导该结果，以使其与其他定义保持一致，并将原始结果扩展到确定性子句理论。

3.2.2 负例自底向上预处理

自底向上预处理生成两组不同的假设约束。一组通过对 LFF 问题中反例的自底子句进行预处理生成，另一组通过对正例的自底子句进行预处理生成。本小节将负例自底向上预处理 定义为从反例生成假设约束的方法。

3.2.3 正例自底向上预处理

本小节定义了正例自底向上预处理 ，即自底向上预处理方法中从 ILP 问题的正例生成假设约束的部分。

山本[30] 提出的经典例子说明了子和在逆蕴涵中的不完备性，后来被 Muggleton[21] 更新为无函数形式。具体如下：

为了表征自底子句，其他方法被设计出来，这些方法可以在自底子句和空子句之间的子和格之外找到假设[26]。本文使用了逆蕴涵和原始论文[20]中给出的自底子句，并承认其不完备性。在未来的工作中，可以尝试利用对逆蕴涵的改进来生成正例的假设约束。

逆蕴涵的不完备性意味着正例自底向上预处理是不可靠的（unsound）。然而，可以证明正例自底向上预处理不会修剪由相对子和（relative subsumption）定义的一个特定子集的假设[25]。

因此，正例自底向上预处理不会修剪 ILP 问题解集中一个定义明确的子集。然而，无法保证问题存在一个子和完备（subsumption-complete）的解。因此，正例自底向上预处理可能会修剪掉所有解，并且不能保证保留最优解。这一问题对正例自底向上预处理的影响程度将在第 5 章中通过实验进行探讨。

3.2.4 自底向上预处理的定义

在定义了正例预处理和反例预处理之后，现在可以给出自底向上预处理的完整定义。

3.3 泛化关系

自底向上预处理的核心是一种基于子和（subsumption）的泛化关系。子句之间的子和测试是 NP 完全问题[8]。第 5 章通过实验表明，对于复杂的 ILP 问题，完整的子和检查有时会显著增加学习时间。本章的其余部分将证明，在不修剪额外解的前提下，可以如何弱化自底向上预处理所使用的泛化关系。

3.3.1 负例自底向上预处理

命题 4 表明，只要使用一种可靠的泛化关系，负例自底向上预处理就是可靠的。这意味着该泛化关系可以是不完备的，并且可能会将某些泛化错误地分类为非泛化。这种极端情况的一个例子可能是一个始终返回假的泛化关系，即它假设没有任何东西是泛化。

3.3.2 正例自底向上预处理

根据命题 5 ，使用一个完备的泛化定义足以确保正例自底向上预处理不会修剪子和完备的解。在极端情况下，一个完备的泛化关系可能会始终返回真，即它假设一切都是泛化。第 4 章表明，有用的完备泛化关系比可靠但不完备的泛化关系更难计算。第 5 章的实验表明，即使使用不完备的泛化定义对正例进行自底向上预处理生成的假设约束，在各种问题上仍然只会修剪极少的解。

第四章

⊥-Popper 实现

⊥-Popper 为元级 ILP 系统 Popper[7] 实现了自底向上预处理。本章描述了 ⊥-Popper 的实现。虽然 ⊥-Popper 是一个特定的实现，但这里描述的技术可以适配到其他支持假设约束的元级 ILP 系统。

备注 ：本章中的背景知识（BK）假定是用 Prolog 编写的。它不保证具有有限的 Herbrand 基。Prolog 还支持“作为失败的否定”（negation as failure）。这可能导致 Prolog 程序是非单调的。假定背景知识被编写为一个确定性程序。

4.1 概述

4.1.2 L: 假设语言

Popper 中的假设约束是用 ASP（答案集编程）编写的。这使得 ⊥-Popper 能够充分利用 ASP 的表达能力来编写假设约束、泛化关系以及自底子句编码。

Popper 使用以下谓词符号在 ASP 中编码猜测的假设：

  • head_literal/2
  • body_literal/2

⊥-Popper 通过对涉及这些谓词符号和 clause/1 的事实进行约束编码，从而修剪假设空间。本节简要描述了该编码方式。完整编码的细节可以在 Popper 论文[7]的第 4 章中找到。

4.1.3 自底子句编码

⊥-Popper 为每个自底子句编码多个自底子句变体。选择自底子句变体的细节将在第 4.4 节中给出。在此，定义了自底子句变体，并解释了它们的编码方式。

4.2 hyp_constraints : 假设约束

⊥-Popper 的假设约束是按照定义 31 中给出的自底向上预处理的直接 ASP 编码。该 ASP 代码在算法 2 中给出。符号 _ 是一个匿名变量。如果 generalizes_bottom_clause(_, D) 成立，那么当前猜测的假设中存在某个子句 Cl，使得 generalizes_bottom_clause(Cl, D) 成立。换句话说，如果 generalizes_bottom_clause(_, D) 成立，则当前假设 H是 D的泛化。

第 3 项在计算上具有挑战性，因为子和检查是 NP 完全问题。
下一节关于 gen_rels 的内容描述了 generalizes_bottom_clause/2 的一种子和可靠（subsumption-sound）的实现方式。
关于 bc_enc 的部分展示了如何通过编码自底子句的多种变体来提高 generalizes_bottom_clause/2 的覆盖范围，使其接近子和完备性（subsumption-completeness）。

组件 gen_rels 的 ASP 代码在算法 3 中给出。当一个自底子句被编码为与其自身相等的单一变体时，generalizes_bottom_clause/2 等价于 sound_gen/2。因此，在这种情况下，generalizes_bottom_clause/2 是子和可靠的（subsumption-sound）。当 bc_enc 是完备的时，generalizes_bottom_clause/2 等价于 complete_gen/2。因此，gen_rels 的子和完备性与子和可靠性取决于 bc_enc 所编码的自底子句变体。

4.4 bc_enc : 自底子句编码

bc_enc 是一个组件，它从每个自底子句生成多个自底子句变体并将它们编码到 L中。理想情况下，这种方法可以确保 gen_rels 同时具备子和可靠性（subsumption-sound）和子和完备性（subsumption-complete）。

当 ⊥B(e) 针对某个事实 e 被提升到变量时，假设 ⊥B(e) 中出现的任何相同的基础项（ground term）都应该被提升为相同的变量。例如，一个基础原子 middle([], []) 可能会被提升为原子 middle(A, A)。如果 ⊥B,L(e) 然后是 palindrome(A):- middle(A, A)，那么子句 palindrome(A):- middle(A, B) 通过替换 θ = {B/A} 泛化了 ⊥B,L(e)。

原始的 Progol 实现通过在其搜索过程中执行一种称为变量分裂 （variable splitting）的技术来处理这种情况 [20]。后来的系统如 Aleph 和 ATOM 则在底子句（bottom clause）上执行变量分裂 [1]。

为了描述变量分裂，首先需要定义一个字面量中变量的方向。假设 L 是一种语言偏置（language bias）。假设 C 是一个子句。假设 Vi 是出现在字面量 a ∈ C 中的一个变量，其形式为 p(V1, V2, · · · , Vn)。假设存在一个方向声明（direction declaration），其形式为 direction(p, (D1, D2, · · · , Dn)) ∈ Ld。那么 Vi 在 a 中具有方向 Di。根据方向声明的定义，Di 要么是 in，要么是 out。

在 L 下对子句 C 进行变量分裂会生成一个子句 CV S，遵循以下算法：

变量分裂确保在 CV S 中所有方向为 out 的变量都是唯一的。当一个复制的字面量被进一步拆分时，它还可能向底子句添加大量额外的字面量。

如果在变量分裂过程中变量 V′ 被添加到 V 的等价类中，Aleph 和 ATOM 会在底子句中添加相等性字面量 V = V′。因此，例如 C = palindrome(A):- middle(A, A) 在变量分裂后可能会变成 CV S = palindrome(A):- middle(A, B), A = B。然后，CV S 中字面量的任何子集在逻辑上都等价于 C 的一种泛化。

bc_enc 采用了一种略有不同的方法。假设 C 是一个子句，CV S 是 C 经过变量分裂后的结果。假设 V = {V0, V1, · · · , Vn} 是 CV S 中所有唯一变量的集合。bc_enc 为 V 中变量到 V 的子集的所有可能替换 θ 编码一个底子句变体，其中 θ 中的 Vi/Vk 和 Vj/Vk 仅在 Vj ∈ [[Vi]] 时成立。换句话说，在 θ 中，Vi 和 Vj 只有在变量分裂过程中被添加到同一个等价类时，才能映射到相同的变量。

在研究这个问题时，我曾认为变量分裂会使 bc_enc 在子句包含关系（subsumption）上是完备的。具体来说，我认为以下命题是成立的：假设 C 和 D 是针对某种语言偏置 L 的偏置一致子句（bias consistent clauses）。假设 DV S 是 D 经过变量分裂后的结果。如果存在某个替换 θ 使得 Cθ ⊆ D，则存在一个替换 θ′ 使得 C ⊆ DV Sθ′。

然而，在 Tamaddoni-Nezhad 和 Muggleton 关于 Progol 的细化算子完备性的一篇论文中，给出了一个反例 [28]。假设 D 是 palindrome(A):- middle(A, A)，而根据变量分裂算法，DV S 是 palindrome(A):- middle(A, B)。再假设 D′ = palindrome(A):- middle(A, B), middle(B, A)。那么 D′ 包含 D，但不存在任何替换 θ 使得 D′ ⊆ DV Sθ。可以认为 D′ 是冗余的，因为它在逻辑上等价于 D，因此永远不会出现在最优解中。

尽管如此，这个例子仍然引发了对这种底子句编码方法完备性的质疑。我未能完成一个足够强有力的证明以包含在此处。第 5 章的实验表明，即使 generalizes_bottom_clause/2 在此 bc_enc 实现中不是一个完备的泛化关系，它在实践中至少表现良好。在第 7 章的局限性部分，我简要描述了几种改进正向底子句预处理泛化关系实现的方法，以克服这一潜在限制。

bc_enc 按照以下步骤编码底子句变体：

在许多情况下，只要有足够的示例，即使不使用变量分裂也可以找到目标假设。然而，也有一些问题必须使用变量分裂才能找到目标假设 [28]。⊥-Popper 可以选择启用或禁用变量分裂。如果禁用变量分裂，则 ⊥V S B,L(e) = ⊥B,L(e)，并且 T 中的替换是一对一的。第 5 章的实验表明，变量分裂可能会显著增加学习时间，并且通常并不是找到最优解所必需的。

4.4.1 替换的优化

4.5 bc_prog : 底子句生成

到目前为止，本章已经展示了如何从示例的底子句中生成符合子句包含关系（subsumption-sound）的假设约束。接下来需要描述最后一个组件 bc_prog ，它为 LFF 问题输入中的每个示例构建一个底子句。

当问题的背景知识（BK）是一个 Datalog 程序时，可以通过计算 B ∪ ¬e 的最小 Herbrand 模型来确定示例的底子句 [8]。由于 B ∪ ⊥B(e) |= e，因此必然有 B ∪ ¬e |= ¬⊥B(e)。如果 B ∪ ¬e 的最小 Herbrand 模型是一组基础事实 b₁ ∧ b₂ ∧ · · · ∧ bn，则 ⊥B(e) 是 ¬(¬e ∧ b₁ ∧ b₂ ∧ · · · ∧ bn)。这意味着 ⊥B(e) 是子句 e ← b₁, b₂, ..., bn。需要注意的是，这种使用否定的方式之所以有效，是因为 e 和所有 bi 都是事实。该算法可以称为基于前向链的底子句构造（Bottom Clause Construction with Forward Chaining），或简称为 BCF C ，因为 Datalog 程序的最小 Herbrand 模型可以通过前向链算法计算 [8]。

然而，当 BK 用 Prolog 编写时，BCF C 存在两个问题。首先，Prolog 不保证具有有限的 Herbrand 基础，因此计算最小 Herbrand 模型可能是无限的。其次，如果 BK 中的子句不是范围受限的（range-restricted），即它们的头部包含不存在于体部的变量，则前向链可能会失败。由于 Popper 允许使用 Prolog 的 BK，⊥-Popper 转而采用原始逆蕴涵论文 [20] 中给出的底子句构造算法，称为 BCIE 。与 BCF C 相比，BCIE 更高效，并且能够直接计算示例的偏置一致底子句（bias consistent bottom clause）。然而，BCIE 比 BCF C 显得复杂得多。

bc_prog 在大约 200 行 Prolog 代码中实现了 BCIE 。由于 BCIE 已被广泛研究，其正确性证明已在原始论文中给出，因此这里省略了完整描述。用于在 ⊥-Popper 中执行底子句构造的代码可以在附录 B 中找到。附录 A 还提供了一个程序，将定义 6 中给出的 LFF 语言偏置转换为模式声明（mode declarations）。由此可知，bc_prog 构造偏置一致底子句的事实直接来源于 BCIE 构造模式一致底子句的证明。

为了确保底子句构造终止，BCIE 使用了一个称为变量深度 （variable depth）的概念对其进行了限制。

定义 35（变量深度）

如果 C 是一个子句，V = {v₁, v₂, · · · , vn} 是出现在 C 中的所有唯一变量的集合，则变量 vi ∈ V 的变量深度（depth(vi)）定义如下：

假设 M 是语言偏置 L 中的模式声明集合，j⁺ 和 j⁻ 分别是 M 中任何模式声明中输入变量和输出变量的最大数量，r 是 M 中任何模式声明中的最大召回值（recall），i 是最大变量深度（max_variable_depth）。正如原始论文 [20] 中所述，BCIE 的计算复杂度被限制在 (j⁺j⁻r|M|)ᵢⱼ⁺。因此，在理论上，⊥-Popper 中的底子句构造在语言偏置的规模或 max_vars 的值较大时可能会表现较差。然而，实践中这很少成为问题，这一点将在第 5 章中展示。

通常情况下，在 Popper 问题中，max_vars 默认为 5，因此 i = 4。典型情况下，j⁺ ≤ 2。由于召回值（recall）默认为 ∗，r 可能是无限的，但项 j⁺j⁻r 也受到深度为 i 的最小 Herbrand 模型中真原子数量的限制，而这个数量通常相当小。

4.6 递归约束

命题 7 证明了 Popper 生成的任何假设都不可能包含变量深度大于 max_vars - 1 的子句。然而，如果一个假设可以自我解析（self-resolve），那么多次自我解析的结果可能会生成一个子句，其中变量的深度超过理论中变量的总数。出于这个原因，⊥-Popper 对递归理论的剪枝比其他理论更加谨慎。

算法 4 包含了额外的假设约束，这些约束在允许递归的问题中放宽了 generalizes_bottom_clause/2 的限制。假设 C 是形式为 h ← b₁, · · · , bn 的子句，其中某个 br（1 ≤ r ≤ n）具有与 h 相同的谓词符号，则 C 是一个递归子句。假设 k 是 br 中输入变量的最小变量深度。如果字面量 bi 中的所有输出变量 Vj 满足 depth(Vj) < k，则称字面量 bi 在递归之前出现。

当底子句从正例构造且问题支持递归时，算法 4 中的约束为 generalizes_bottom_clause/2 添加了一个额外的情况。在这种情况下，对于一个子句 C 和一个正底子句变体 D，如果 C 中所有在递归之前出现的字面量的子集（记为 Cr）是 D 的子集，则 generalizes_bottom_clause(C, D) 成立。这使得 generalizes_bottom_clause/2 在递归问题的正向底预处理过程中成为一个不健全的泛化关系。然而，在这种情况下，generalizes_bottom_clause/2 仍然可以是一个完备的泛化关系。命题 5 表明，这一条件足以保证正向底预处理保持子句包含关系的正确性。

需要注意的是，算法 4 需要对未定义的谓词符号 var_direction/4 进行某种定义。假设 var_direction(P, Vars, Dir, Var) 成立，当且仅当 Vars 具有形式 (V₁, · · · , Vn)，Var 是某个 Vi，并且问题的语言偏置中形式为 direction(P, (D₁, · · · , Dn)) 的方向声明满足 Di = Dir。然后，算法 4 编码了这一限制。

https://arxiv.org/pdf/2112.12551