文章目录
承前
基本原理
Robinson的基本方法
命题逻辑中的归结原理
谓词逻辑中的归结原理
归结原理推论1（充分）
归结原理推论2（充要）
重要

承前
谓词公式的不可满足性分析可通过把谓词公式转化为子句集后，对子句集中的子句作不可满足性分析
基本原理
因为子句集中的子句是合取关系，所以如果一个子句集中存在空子句，则此子句集不可满足。
Robinson的基本方法
检查子句集S中是否包含空子句，若包含，则其不可满足，若不包含，则在子句集中选择合适的子句进行归结，一旦通过归结得到了空子句，则S不可满足
命题逻辑中的归结原理


归结式C12是其亲本子句C1与C2的逻辑结论，即：

如果C1与C2为真，则C12为真

谓词逻辑中的归结原理
由于谓词逻辑的子句中含有变元，所以不像命题逻辑那样可以直接消去互补文字，而需要先用最一般合一对变元进行代换，然后才能进行归结



如果两个子句分别为P(x)或Q(a)和非P(y)或R(y)，则这两个子句不能进行归结，因为两个子句中的P均含变量

如下：不能对P(x)和非P(y)进行归结


归结原理推论1（充分）

归结原理推论2（充要）



重要
如果归结出了空子句，则子句集不可满足。但如果没有归结出空子句，则既不能说子句集不可满足，也不能说子句集可满足

一、预备知识




两个合式公式等价（真值表相同）关系表




否否：~ (~P) $\Leftrightarrow$ P


 P $\to$ Q $\Leftrightarrow$ ~P $\vee$ Q


狄摩根定律： ~(A$\vee$B) $\Leftrightarrow$ ~A $\wedge$ ~B      ~(A$\wedge$B) $\Leftrightarrow$ ~A $\vee$ ~B


分配律：P $\wedge$ (Q$\vee$R) $\Leftrightarrow$ (P$\wedge$Q) $\vee$ (P$\wedge$R)  P $\vee$ (Q$\wedge$R) $\Leftrightarrow$ (P$\vee$Q) $\wedge$ (P$\vee$R)


交换律：P $\wedge$ Q $\Leftrightarrow$ Q $\wedge$ P     P $\vee$ Q $\Leftrightarrow$ Q $\vee$ P


结合律：(P$\wedge$Q) $\wedge$ R $\Leftrightarrow$ P $\wedge$ (Q$\wedge$R)  (P$\vee$Q) $\vee$ R $\Leftrightarrow$ P $\vee$ (Q$\vee$R )


逆否律：P $\to$ Q $\Leftrightarrow$ ~Q $\to$ ~P


~ ($\exists x$) P(x) $\Leftrightarrow$ ($\forall x$) (~P(x))  ~ ($\forall x$) P(x) $\Leftrightarrow$ ($\exists x$) (~P(x))


($\forall x$) (P(x) $\wedge$ Q(x)) $\Leftrightarrow$ ($\forall x$) P(x) $\wedge$ ($\forall x$) Q(x)   ($\exists x$) (P(x) $\vee$ Q(x)) $\Leftrightarrow$ ($\exists x$) P(x) $\vee$ ($\exists x$) Q(x)


($\forall x$) P(x) $\Leftrightarrow$ ($\forall y$) P(y)   ($\exists x$) P(x) $\Leftrightarrow$ ($\exists y$) P(y)






父辈字句
消解式




P和~P∨ Q（即P→Q）
Q


P ∨ Q 和~P ∨ Q
Q


P ∨ Q和~ P ∨ ~ Q
Q ∨ ~Q和P ∨ ~P


~P和P
NIL


~P ∨ Q（即P→Q）和   ~Q ∨ R（即Q→R）
~P ∨ R（即P→R）


B(x)和~B(x) ∨ C(x)
C(x)


P(x) ∨ Q(x)和~Q( f(y) )
P( f(y) )，σ={ f(y) / x }


P(x, f(y)) ∨ Q(x) ∨ R(f(a), y)和~P(f(f(a))，z) ∨ R(z,w)
Q(f(f(a))) ∨ R(f(a), y) ∨ R(f(y), w), σ={f(f(a)) /x,f(y)/z } [BG]F


二、利用消解法证明可以从下述的前提推到结论
前提：每个储蓄钱的人都获得利息

结论：如果没有利息，那么就没有人去储蓄钱

提示:可按照下述步骤进行实验
1.规定原子公式
S(x, y)     表示 “x储蓄y”
M(x)        表示 “x是钱”
I(x)        表示 “x是利息”
E(x, y)     表示 “x获得y”

2.基于原子公式表示前提和结论
前提：
结论：
3.把前提化为字句型
①消去蕴含符号：
②减少否定符号的辖域：


③对变量标准化：
④消去存在量词：令z=f(x)为Skolem函数，则可得字句形如下：
⑤化为前束形：
⑥把母式化为合取范式：
⑦消去全称量词：
⑧消去连词符号：
⑨更换变量名称：
4.将结论的否定化为子句型
结论的否定：
化为字句形：

①消去蕴含符号：
②减少否定符号的辖域：





③对变量标准化：
④消去存在量词：
⑤化为前束形：

⑥把母式化为合取范式：

⑦消去全称量词：
⑧消去连词符号：
⑨更换变量名称：
5.基于3和4的字句型集，画出消解树，推导到NIL
子句型集：
消解（归结）：






由(2)f(x)/z



由(1)(3)






 由(5)x/a，y/b



由(4)(6),b/y(y/b)






由(7)(8)

写出利用归结原理求解问题答案的步骤
（1）写出谓词关系公式。（2）用反演法写出谓词表达式。（3）SKOLEM标准形式。（4）命题表示成合取范式并求子句集S。（5）将结论否定并加入S中，对S中可归结的子句做归结。（6）归结式仍放入S中，反复归结过程。（7）得到空子句。（8）得证。

归结原理给出了证明子句集不可满足性的方法。

如欲证明Q为P1,P2,…,Pn的逻辑结论，只需证 (P1∧P2∧…∧Pn)∧¬Q 是不可满足的。

应用归结原理证明定理的过程称为归结反演。 设F为已知前提的公式集，Q为目标公式(结论)，用归结反演证明Q为真的步骤是：

1.否定Q，得到¬Q；

2.把¬Q并入到公式集F中，得到{F, ¬Q};

3.把公式集{F, ¬Q}化为子句集S；

4.应用归结原理对子句集S中的子句进行归结，并把每次归结得到的归结式都并入S中。如此反复进行，若出现了空子句，则停止归结（不论是否还剩余子句集），此时就证明了Q为真。


注意：此时归结完成后（2）并没有进行归结，但是已经出现了空子句，那么就应停止归结。