我在理解《人工智能现代方法》一书中关于一阶逻辑推理的以下段落时遇到了一些困难：
命题化技术可以完全通用；也就是说，每个一阶知识库和查询都可以以保留蕴涵的方式进行命题化。因此，我们有一个完整的蕴涵决策程序......或者可能没有。有一个问题：当知识库包含一个函数符号时，可能的基础术语替换的集合是无限的！例如，如果知识库提到了父亲符号，则可以构造无限多个嵌套术语，例如父亲(Father(Father(John))) 。我们的命题算法将难以处理无限大的句子集。
幸运的是，由于 Jacques Herbrand（1930）有一个著名的定理，即如果一个句子被原始的一阶知识库所蕴涵，那么就有一个证明只涉及命题化知识库的有限子集。任何这样的子集在它的基本术语中都有最大的嵌套深度，我们可以找到子集 y 首先生成所有具有常量符号（理查德和约翰）的实例，然后是深度为 1 的所有术语（父亲（理查德）和父亲（约翰） )，然后是深度为 2 的所有项，依此类推，直到我们能够构造出蕴涵句子的命题证明。
我知道在替换过程中会产生无限的嵌套项——但是下一段谈论这个定理完全超出了我的想象。