简化到命题推理

9.1.2 简化到命题推理

一旦我们有了从量化语句推导非量化语句的规则，就可能将一阶推理简化为命题推理。在本节中，我们将介绍主要的思想；具体内容将在第9.5节中介绍。

第一种思想是：正如存在量化语句能被某个实例化取代一样，全称量化语句也可以被所有可能的实例化集代替。例如，假设我们的知识库仅仅包括如下语句：

然后我们使用知识库的词汇表中所有可能的基项，把UI规则应用于第一个语句，即{x / John}和{x /Richard}。我们得到

然后我们可以丢弃全称量化语句。现在，如果我们把基本原子语句——King(John)，Greedy(John)，等等——看作命题符号，知识库本质上就是命题逻辑了。因此，我们可以使用第七章中的任何完备的命题算法获得诸如Evil(John)之类的结论。

正如我们在第 9.5 节中将显示的，这种命题化技术完全可以通用；也就是说，通过保留蕴涵，每个一阶知识库和查询都可以命题化。这样，我们得到一个有关蕴涵的完备判定程序……但也可能得不到。这里存在一个问题：当知识库包含函数符号时，可能的基项置换集将是无限的！例如，如果知识库包括符号Father，那么可以构造无限多个嵌套项，比如Father(Father (Father (John)))。我们的命题算法处理这些无穷大的语句集合有困难。

幸运的是，雅克·海布兰（Jacques Herbrand，1930）对该效应提出了一个著名的定理，这就是如果某个语句被原始的一阶数据库蕴涵，则存在一个只涉及命题化知识库的有限子集的证明。由于任何这样的子集在其基项中都有一个最大嵌套深度，我们可以找到这些子集，首先，生成所有常量符号（Richard和John）的实例化，再生成所有深度为1的项（Father(Richard)和Father(John)），然后是深度为2的项，依此类推，直到我们可以构造出蕴涵语句的命题证明。

我们已经勾画出通过命题化进行一阶推理的完备方法——也就是，任何蕴涵语句都能得到证明。在已知可能模型的空间是无穷的情况下，这是个重要的成果。另一方面，我们并不知道一个语句是被蕴涵的，直到证明完成！如果语句不被蕴涵的话，将会发生什么情况？我们能判断出来吗？当然，对于一阶逻辑，我们不能。我们的证明程序可以不断进行下去，生成越来越深的嵌套项，但是，我们不知道是否陷于无望的循环中，或者证明是否就要出现了。这非常像图灵机的停机问题。阿兰·图灵（1936）和阿隆佐·丘奇（Alonzo Church，1936）用相当不同的方法证明了这种事件状态的必然性。一阶逻辑的蕴涵问题是半可判定的——也就是，存在肯定每个蕴涵语句的算法，而不存在还能否定每个非蕴涵语句的算法。