第三章一阶谓词逻辑.ppt

1. 命题逻辑中的归结原理 定义 设C1与C2是子句集中的任意两个子句，如果C1中的文字L1与C2中的文字L2互补，那么从C1和C2中分别消去L1和L2，并将二个子句中余下的部分析取，构成一个新子句C12，则称这一过程为归结，称C12为C1和C2的归结式，称C1和C2为C12的亲本子句。 设子句 C1=L∨C1’ C2=(﹁L)∨C2’ 则归结式C12=C1’∨C2’ C1和C2为C12的亲本子句。 互补文字的定义 若P是原子谓词公式，则称P与﹁P是互补文字 ﹁P∨Q ﹁Q P Q NIL 举例 设C1=P∨Q∨R C2=﹁P∨S 则归结式C12为 C12=Q∨R∨S 设C1=P C2=﹁P 则归结式C12为 C12=NIL 归结过程的树形表示 例如 C1=﹁P∨Q C2=﹁Q C3=P 求C1 C2C3的归结式C123？ 一. 命题逻辑中的归结原理 定理： 归结式C12是其亲本子句C1和C2的逻辑结论 （C12的值是C1合取C2的值） 即：C1 ∧ C2 ? C12 是一种推理规则 证明：设C1= L∨C1′, C2= ﹁L∨C2′ 通过归结可得到： C12=C1′∨ C2′ 由定义知：C1和C2是C12 的亲本子句 ∵ L ∨ C1′? C1′∨ L C1′∨ L ? ﹁C1′→L ﹁L∨C2′? L→ C2′ ∴ C1 ∧ C2 =(﹁C1′→L) ∧ (L→C2′) 根据假言三假论（P→Q，Q→R ?P→R）得到： (﹁ C1′ →L) ∧ (L →C2′) ? ﹁C1′→C2′ ∵ ﹁C1′→C2′? C1′∨ C2′= C12 ∴ C1 ∧ C2 ? C12 推论1：设C1与C2是子句集S中的两个子句，C12是它们的归结式，若用C12代替C1和C2后得到新子句集S1，则由S1的不可满足性可推出原子句集S的不可满足性。 推论2：设C1与C2是子句集S中的两个子句，C12是它们的归结式，若把C12加入S中，得到新子句集S2，则S与S2在不可满足的意义上是等价的。 从前面的推论中可以看出：要证明子句集S的不可满足性，只要对其中可进行归结的子句进行归结，并把归结式加入子句集S或用归结式替换它的亲本子句，而后，对新子句集证明不可满足性即可，在归结的过程中能得到空子句，立即可得到原子句集S是不可满足的结论。 谓词逻辑与命题逻辑相比是含有变元，需选用最一般合一对变元进行代换，然后才能进行归结。 定义 设C1与C2是两个没有相同变元的子句，L1和L2分别是C1和C2中的文字，若σ是L1和L2的最一般合一，则称 C12=(C1σ — {L1σ})∪(C2σ — {L2σ}) 为C1和C2的二元归结式，L1和L2称为归结式的文字。 二.谓词逻辑的归结原理 例1 设 C1=P(a)∨﹁Q(x)∨R(x) C2=﹁P(y)∨Q(b) 给出C1和C2的归结式。 解 若选L1=P(a), L2=﹁P(y)，则σ ={a / y}是L1与﹁L2的最一般合一, 根据定义，可得： C12 =(C1σ — {L1σ})∪(C2σ — {L2σ}) =({P(a), ﹁Q(x), R(x)}—{P(a)})∪({﹁P(a), Q(b)}—{ ﹁P(a)}) =({﹁Q(x), R(x)})∪({Q(b)}) ={﹁Q(x), R(x), Q(B)} =﹁Q(x)∨R(x)∨Q(B) 本例的一种归结树 P(A) ∨ ﹁ Q(x)∨R(x) ﹁ P(y)∨Q(B) Q(x)∨R(x) ∨Q(B) {A/y} 若选L1= ﹁ Q(x), L2=Q(b), σ={b/x}, 则可得： C12 =({P(a), ﹁ Q(b), R(b)}—{﹁ Q(b)})∪({﹁ P(y), Q(b)}—{Q(b)}) =({P(a), R(b)})∪({﹁P(y)}) ={P(a), R(b), ﹁P(y)} =P(a)∨R(b)∨﹁P(y) 另一种归结树 P(a) ∨ ﹁ Q(x)∨R(x) ﹁ P(y)∨Q(b) P(a)∨R(b) ∨ ﹁ P(y) {b/x} 解 由于C1与C2有相同的变元，不符合定义的要求。为了进行归结，需修改C2中变元的名字，令C2=﹁P(B)∨R(y)。此时，对C1和C2有 L1 =P(x), L2=﹁P(B) L1与﹁L2的最一般合一σ={