谓词逻辑归结原理

归结法基本原理

归结法的基本原理是采用反证法（也称反演推理法）将待证明的表达式（定理）转换成为逻辑公式（谓词公式），然后再进行归结，归结能够顺利完成，证明原公式（定理）是正确的。

def: Q 为 P_1,P_2, \cdots ,P_n 的逻辑结论，当且仅当 P\wedge \neg Q 是不可满足的，结论才成立

这样做的原因是证明不可满足性要比证明可满足性简单得多。通俗来讲，若要证明定理：张三是个好人。可以反向证明定理：张三不是个好人那是不可能的。

用符号公式表示就是:

置换转换为普通谓词公式:

再将其否定：

谓词逻辑归结原理

子句集

为了描述子句集，先给出如下几个名词的定义：

• 原子谓词公式：一个不能再分解的命题
• 文字：原子谓词公司及其否定 P: 正文字 \neg P: 负文字
• 子句：任何文字的 析取式，任何文字本身也都是句子。
• 空子句：不包含任何文字的子句
• 子句集：所有子句的集合

例 1： 将下列谓词公式化为子句集

A. 利用一下公式消去谓词公式中的

P\rightarrow Q\Leftrightarrow \neg P\vee Q,P\leftrightarrow Q\Leftrightarrow (P\wedge Q)\vee (\neg P\wedge \neg Q)

\color{red}{\Longleftrightarrow} \forall x (\neg \forall yP(x,y) \vee \neg \forall y(\neg Q(x,y)\vee R(x,y))) B. 利用下列公式把否定符号 \neg 移到紧靠谓词的位置上

双重否定律：\neg (\neg P)\Leftrightarrow P 摩根律：\neg (p\wedge q)\Leftrightarrow \neg p\vee \neg q 量词否定转换率：\neg \exists xP\Leftrightarrow \forall x\neg P,\neg \forall xP\Leftrightarrow \exists x \neg P

\color{red}{\Longleftrightarrow} \forall x(\exists y\neg P(x,y)\vee \exists y(Q(x,y)\wedge \neg R(x,y))) C. 变量标准化(变元易名)

\exists xP(x) = \exists yP(y),\forall xP(x) = \forall yP(y)

\color{red}{\Longleftrightarrow} \forall x(\exists y\neg P(x,y)\vee \exists \color{green}{z}(Q(x,\color{green}{z})\wedge \neg R(x,\color{green}{z})))

D. 消去存在量词（两种情况）

a. 存在量词不出现在全称量词的辖域内 b. 存在量词出现在一个或者多个全称量词的辖域内 对于一般情况： \forall x_1(\forall x_2(\cdots \forall x_n(\exists yP(x_1,x_2,\cdots ,x_n,y)))\cdots) 存在量词 y 的 Skolem 函数为 y=f(x_1,x_2,\cdots ,x_n) Skolem 化：用 Slolem 函数代替每个存在量词化的变量的过程

如本例中两个存在量词 y,z 只收到全称量词 x 的约束，因此可以令：y = f(x),z = g(x) \color{red}{\Longleftrightarrow} \forall x(\neg P(x,\color{green}{f(x)})\vee (Q(x,\color{green}{g(x)})\wedge \neg R(x,\color{green}{g(x)})))

E. 化为前束范式（本例中到此式子已经满足前束范式标准了）

\color{red}{\Longleftrightarrow} \forall x(\neg P(x,\color{green}{f(x)})\vee (Q(x,\color{green}{g(x)})\wedge \neg R(x,\color{green}{g(x)})))

F. 化为 Skolem 标准型

Skolem 标准型： M: 子句的合取式，称为 Skolem 标准型的母式，即去掉所有量词的前束范式。 利用分配律： p\vee(q\wedge r)\Leftrightarrow (p\vee q)\wedge (p\vee r) p\wedge(q\vee r)\Leftrightarrow (p\wedge q)\vee (p\wedge r)

\color{red}{\Longleftrightarrow} \forall x((\neg P(x,\color{green}{f(x)})\vee Q(x,\color{green}{g(x)}))\wedge (\neg P(x,\color{green}{f(x)})\vee \neg R(x,\color{green}{g(x)})))

G. 略去全称量词 \color{red}{\Longleftrightarrow} ((\neg P(x,\color{green}{f(x)})\vee Q(x,\color{green}{g(x)}))\wedge (\neg P(x,\color{green}{f(x)})\vee \neg R(x,\color{green}{g(x)})))

H. 消去合取词, 成为一个子句集合（析取句的集合） \color{red}{\Longleftrightarrow} {(\neg P(x,\color{green}{f(x)})\vee Q(x,\color{green}{g(x)}), \neg P(x,\color{green}{f(x)})\vee \neg R(x,\color{green}{g(x)})}

I. 子句变量的标准化（不同子句用不同变元） \color{red}{\Longleftrightarrow} {(\neg P(x,\color{green}{f(x)})\vee Q(x,\color{green}{g(x)}), \neg P(y,\color{green}{f(y)})\vee \neg R(y,\color{green}{g(y)})}

鲁滨逊归结原理(判别子句集的不可满足性)

出发点：由于子句集当中的子句之间的关系是合取关系，因此只要有一个子句不可满足，则整个子句集就不可满足。

⭐️鲁滨逊归结原理的基本思想：

• 检查子句集 S 中是否包含 空子句，若包含，则不可满足。
• 若不包含空子句，在 S 中选择合适的子句进行归结，一旦归结出空子句，就说明 S 是不可满足的。
• 另外需注意的是，对于鲁滨逊归结原理，如果在归结过程中出现空子句则可说明子句集的不可满足性；但若无法归结出空子句也无法说明该子句集可满足，也就是说鲁滨逊归结原理只能用来证伪。

命题逻辑中的归结原理： Def: 归结指的是，设 C_1 与 C_2 是子句集中的任意两个句子，如果 C_1 中的文字 L_1 与 C_2 中的文字 L_2 互补 (同一谓词的正负文字)，那么从 C_1 与 C_2 中分别消去 L_1 和 L_2, 并将两个子句中余下的部分 析取，构成一个新的子句 C12。 Def: 归结式 C12 是其亲本子句 C_1 和 C_2 的逻辑结论。即如果 C_1 与 C_2 为真，则 C12 为真。 推论 1： 由 C12 代替 C_1 和 C_2 后的新的子句集 S_1 的不可满足性也可代表原子句集的不可满足性（单向的）。 推论 2： 若不作代替，直接将 C12 加入原子句集 S 得到新的子句集 S_2, 则 S 与 S_2 在不可满足的意义上是等价的（双向的）。

谓词逻辑归结原理

⭐️谓词逻辑中的归结原理：（含有变量的子句的归结）

  谓词逻辑的归结比命题逻辑的归结要复杂得多，其中一个原因就是谓词逻辑公式中含有个体变量与函数。因此寻找互补的子句的过程就比较复杂。例如：

就不易从直接比较中发现这两个子句中含有的互补对，但如果将

置换与合一：（对个体变量做适当替换）

置换： 将子句中的变量做适当替换，可替换成常量、变量、Skolem 函数。 合一： 寻找相对变量的置换，使两个谓词公式一致

如： C_1=P(x)\vee Q(a), C_2=\neg P(b)\vee R(x) 解： \sigma = f(a)/x ; x 用 f(a) 替换 C_1\sigma = P(f(a))\vee Q(f(a)), 选互补对：L_1=P(f(a)),L_2=\neg P(y), \sigma = f(a)/y 得归结式：C_12=R(b)\vee Q(f(a))