失败否定式和稳定模型语义

10.7.2 失败否定式和稳定模型语义

在第七章和第九章中，我们看到霍恩范式知识库具备理想的计算属性。然而在许多应用中，一个子句体内的每个文字都是正的，这个要求非常不方便。我们愿意说“You can go outside if it’s not raining （你可以外出，如果没在下雨）”，而不需要编造像NotRaining（未下雨）这样的谓词。本节中，我们探索使用失败否定式的思想，把明确的否定式形式添加到霍恩子句中。这个思想是一个否定文字，not P，在P的证明失败的情况下，能够被“证明”是正确的。这是一种和封闭世界假设有密切相关的缺省推理形式：我们假设某事物如果不能被证明为真时，它就为假。我们用“not”来区分失败否定式和逻辑的“¬”运算。

Prolog允许在子句的体中出现not。例如，考虑下面的Prolog程序：

第1条规则说如果我们在计算机上有一个硬盘驱动器且不是SCSI的，那么它肯定是IDE的。第2条说如果它不是IDE的，则它肯定是SCSI的。第3条说有一个SCSI驱动器暗示有一个SCSI控制器，第4条说我们确实有一个驱动器。这个程序有两个最小模型：

M1= {Drive, IDEdrive}

M2= {Drive, SCSIdrive, SCSIcontroller }

最小模型没有捕捉到使用失败否定式的程序的预期语义。考虑程序

这有两个最小模型，{P}和{Q}。从一阶逻辑观点来看这是有意义的，因为P ⇐ ¬Q与P∨Q等价。但是从Prolog观点来看，这是令人烦恼的：Q从来没有在箭头的左边出现过，那么它怎么能称为一个结果呢？

一个替换方法是稳定模型的思想，这是一个最小模型，模型中的每个原子都有一条准则：即一条规则，头是原子而且其体内的每个文字都是被满足的。技术上，我们说M是程序H的一个稳定模型，如果M是H关于M的约化（reduct）的唯一最小模型。程序H的约化被定义为：首先从H删除体内包含文字not A的任何规则，其中A在模型中，然后删除剩余规则中的任何否定文字。因为H的约化现在是霍恩子句的一个列表，所以它肯定有一个唯一的最小模型。

P ← not Q关于{P}的约化是P，它有最小模型是{P}。因此{P}是一个稳定模型。关于{Q}的约化是一个空程序，有最小模型{}。因此{Q}不是一个稳定模型，由于在公式(10.5)中Q没有准则。作为另一个例子，公式(10.4)关于M1的约化如下：

IDEdrive ← Drive

SCSIcontroller ← SCSIdrive

Drive

这有最小模型M1，所以M1是一个稳定模型。解集程序设计是一种具有失败否定式的逻辑程序设计，它的工作方式是通过把逻辑程序转变成基范式，然后用命题模型检验技术来搜索稳定模型（也就是通常所说的解集）。这样的解集程序设计是 Prolog和类似 WALKSAT 这样的快速命题可满足性证明机的共同后裔。事实上，解集程序设计已经被成功地应用到规划问题中，正如命题可满足性证明机已经做到的那样。解集程序设计相对于其它规划器的优点是灵活程度：规划操作和约束可以用逻辑程序来表达，并且不受特殊规划形式化表示的受限格式的限制。解集程序设计的缺点同其它命题技术一样：如果全域内有很多对象，那么就会出现指数级的速度下降。