一阶逻辑推理的混乱

Question

我在理解《人工智能一种现代方法》一书中关于一阶逻辑推理的以下段落时遇到了一些困难：

命题化技术可以完全通用；也就是说，每个一阶知识库和查询都可以以保留蕴涵的方式进行命题化。因此，我们有一个完整的蕴涵决策程序......或者可能没有。有一个问题：当知识库包含一个函数符号时，可能的基础术语替换的集合是无限的！例如，如果知识库提到Father 符号，则可以构造无限多个嵌套项，例如Father(Father(Father(John)))。我们的命题算法将难以处理无限大的句子集。

幸运的是，由于 Jacques Herbrand（1930）有一个著名的定理，即如果一个句子被原始的一阶知识库所蕴涵，那么有一个证明只涉及一个 有限 em> 命题化知识库的子集。由于任何这样的子集在其基本术语之间具有最大嵌套深度，我们可以找到子集 y 首先生成具有常量符号的所有实例化（Richard 和 John)，然后是深度 1 的所有项（Father(Richard) 和 Father(John)），然后是深度 2 的所有项，依此类推, 直到我们能够构建蕴涵句子的命题证明。

---

我知道在替换过程中会生成无限的嵌套项 - 但下一段谈论这个定理完全超出了我的想象。

Answer 1

Herbrand 定理是半可判定的。目标是找到不再满足查询的实例。您从深度 1 开始并继续，直到发现不可满足。 如果可以满足，它可能会无限循环。