avatar

谓词逻辑归结原理

归结法基本原理

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

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

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

用符号公式表示就是:

待证定理:$P \Rightarrow Q$
置换转换为普通谓词公式:

再将其否定:$\neg(\neg P\vee Q) \Leftrightarrow P\wedge \neg Q$
即证明 $P\wedge \neg Q$ 为永假式

归结演绎推理的思路

子句集

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

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

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

A. 利用一下公式消去谓词公式中的$\rightarrow$ 和 $\leftrightarrow$ 符号

$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$在不可满足的意义上是等价的(双向的)。

子句归结

⭐️谓词逻辑中的归结原理:(含有变量的子句的归结)

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

就不易从直接比较中发现这两个子句中含有的互补对,但如果将$x$取值为$a$,这很显然这两个句子中有互补对。

置换与合一:(对个体变量做适当替换)

置换: 将子句中的变量做适当替换,可替换成常量、变量、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))$

文章作者: Liam
文章链接: https://www.ccyh.xyz/p/3027.html
版权声明: 本博客所有文章除特别声明外,均采用 CC BY-NC-SA 4.0 许可协议。转载请注明来自 Liam's Blog
ღ喜欢记得五星好评哦~
打赏
  • 微信
    微信
  • 支付寶
    支付寶

评论