人工智能导论——谓词公式化为子句集详细步骤

Posted 2023-02-16 心无旁骛~

在谓词逻辑中，有下述定义：
原子（atom）谓词公式是一个不能再分解的命题。
原子谓词公式及其否定，统称为文字（literal）。$P$称为正文字，$\neg P$称为负文字。$P$与$\neg P$为互补文字。
任何文字的析取式称为子句（clause）。任何文字本身也是子句。
由子句构成的集合称为子句集。
不包含任何文字的子句称为空子句，表示为NIL。
由于空子句不含有文字，它不能被任何解释满足，所以，空子句是永假的、不可满足的。
在谓词逻辑中，任何一个谓词公式都可以通过应用等价关系及推理规则化成相应的子句集，从而能够比较容易地判定谓词公式的不可满足性。下面结合一个具体的例子，说明把谓词公式化为子句集的步骤。

[例] 将下列谓词公式化为子句集：
$$(\forall x)(\forall y)\mathbf{P}(\mathbf{x},\mathbf{y})\to \neg (\forall y)[\mathbf{Q}(\mathbf{x},\mathbf{y})\to \mathbf{R}(\mathbf{x},\mathbf{y})]$$

(1) 消去谓词公式中的$“\to ”$和$“\leftrightarrow ”$
利用谓词公式的等价关系：
$$\begin{gathered} \mathbf{P}\to \mathbf{Q}⟺\neg P\vee \mathbf{Q} \\ \mathbf{P}⟷\mathbf{Q}⟺(\mathbf{P}\vee \mathbf{Q})\vee (\neg P\vee \neg Q) \end{gathered}$$
上列等式等价变化为：
$$(\forall x)\neg (\forall y)\mathbf{P}(\mathbf{x},\mathbf{y})\vee \neg (\forall y)[\neg Q(\mathbf{x},\mathbf{y})\vee \mathbf{R}(\mathbf{x},\mathbf{y})]$$

(2)把否定符号移到紧靠谓词的位置上
利用谓词公式的等价关系：
双重否定律： $\neg (\neg P)⟺\mathbf{P}$
德摩根律： $\neg (\mathbf{P}\wedge \mathbf{Q})⟺\neg P\vee \neg Q$
        $\neg (\mathbf{P}\vee \mathbf{Q})⟺\neg P\wedge \neg Q$
量词转换律：$\neg (\forall x)\mathbf{P}⟺(\exists x)\neg P$
          $\neg (\exists x)\mathbf{P}⟺(\forall x)\neg P$

把否定符号移到紧靠谓词的位置上，减少了否定符号的辖域。
上列等式变换为：
$$(\forall x)(\exists y)\neg P(\mathbf{x},\mathbf{y})\vee (\exists y)[\mathbf{Q}(\mathbf{x},\mathbf{y})\vee \neg R(\mathbf{x},\mathbf{y})]$$

(3)变量标准化
所谓变量标准化就是重新命名变元，使每个量词采用不同的变元，从而使不同量词的约束变元有不同的名字。这是因为在任一量词辖域内，受到该量词约束的变元为一哑元（虚构变量），它可以在该辖域内被另一个没有出现过的任意变元统一代替，而不改变谓词公式的值。

$$\begin{gathered} (\forall x)\mathbf{P}(\mathbf{x})\equiv (\forall y)\mathbf{P}(\mathbf{y}) \\ (\exists x)\mathbf{P}(\mathbf{x})\equiv (\exists y)\mathbf{P}(\mathbf{y}) \end{gathered}$$
上面等价变换为：
$$(\forall x)(\exists y)\neg P(\mathbf{x},\mathbf{y})\vee (\exists z)[\mathbf{Q}(\mathbf{x},\mathbf{z})\wedge \neg R(\mathbf{x},\mathbf{z})]$$
(4)消去存在量词
分两种情况：
一种情况是存在量词不出现在全称量词的辖域内。此时只要用一个新的个体常量替换受该存在量词约束的变元，就可以消去存在量词。因为如原谓词公式为真，则总能找到一个个体常量，替换后仍然使谓词公式为真。这里的个体常量就是不含变量的$Skolem$函数。

另一种情况是存在量词出现在一个或者多个全称量词的辖域内。此时要用$Skolem$函数替换受该存在量词约束的变元，从而消去存在量词。这里认为所存在的y依赖于x值，它们的依赖关系由Skolem函数所定义。

对于一般情况：
$$(\forall {\mathbf{x}}_1)(\forall {\mathbf{x}}_2)...(\forall {\mathbf{x}}_{\mathbf{n}})(\exists y)\mathbf{P}({\mathbf{x}}_1,{\mathbf{x}}_2,...,{\mathbf{x}}_{\mathbf{n}},\mathbf{y})$$
存在量词$y$的$Skolem$函数记为：
$$\mathbf{y}=\mathbf{f}({\mathbf{x}}_1,{\mathbf{x}}_2,...,{\mathbf{x}}_{\mathbf{n}})$$
可见，$Skolem$函数把每个$x_1,x_2,...,x_n$值，映射到存在的那个$y$。

用$Skolem$函数代替每个存在量词量化的变量的过程称为$Skolem$化。$Skolem$函数所使用的函数符号必须是新的。

对于上面的例子，存在量词$(\exists y)$及$(\exists z)$都位于全称量词$(\forall x)$的辖域内，所以都需要用$Skolem$函数代替。设$y$和$z$的$Skolem$函数分别记为$f(x)$和$g(x)$，则替换后得到
$$(\forall x)\neg P(\mathbf{x},\mathbf{f}(\mathbf{x}))\vee [\mathbf{Q}(\mathbf{x},\mathbf{g}(\mathbf{x}))\wedge \neg R(\mathbf{x},\mathbf{g}(\mathbf{x}))]$$
(5)化为前束形
所谓前束形，就是把所有的全称量词都移到公式的前面，使每个量词的辖域都包括公式后的整个部分，即：
$$前束形=(前缀)母式$$
其中，（前缀）是全称量词串，母式是不含量词的谓词公式。

对上面的例子，因为只有一个全称量词，而且已经位于公式的最左边，所以，这一步不需要做任何工作。
(6)化为$Skolem$标准形
$Skolem$标准形的一般形式是：
$$(\forall {\mathbf{x}}_1)(\forall {\mathbf{x}}_2)...(\forall {\mathbf{x}}_{\mathbf{n}})\mathbf{M}$$
其中，$M$是子句的合取式，称为$Skolem$标准形的母式。

一般利用：
P ∨ ( Q ∧ R ) ⇔ ( P ∨ Q ) ∧ ( P ∨ R ) P ∧