3.2.2命题逻辑中的归结原理 ◆要证明在前提P下结论Q成立,即是证明P→Q永真, 这只须证明P∧_Q不可满足。根据定理1,只须证 明P∧Q的子句集不可满足。由于子句之间是合取 关系,只要有一个子句不可满足,则整个子句集不 可满足。由于空子句是不可满足的,所以如果子句一 集中包含空子句,则该子句集是不可满足的。若子 句集中不包含空子句,则可通过 Robinson提出的归 结原理对子句集进行归结,归结过程保证子句集的 不可满足性不变。一旦归结出空子句,则证明结束 因此,归结原理把定理的证明化为子句集中归结出 空子句的过程
3.2.2 命题逻辑中的归结原理 要证明在前提P下结论Q成立，即是证明P → Q永真， 这只须证明P Q不可满足。根据定理1，只须证 明P Q的子句集不可满足。由于子句之间是合取 关系，只要有一个子句不可满足，则整个子句集不 可满足。由于空子句是不可满足的，所以如果子句 集中包含空子句，则该子句集是不可满足的。若子 句集中不包含空子句，则可通过Robinson提出的归 结原理对子句集进行归结，归结过程保证子句集的 不可满足性不变。一旦归结出空子句，则证明结束。 因此，归结原理把定理的证明化为子句集中归结出 空子句的过程
定义4、设L是一个文字,则称L与为互补 文字。 定义5、设C1、C2是命题逻辑中的两个子句, C1中有文字L1,C2中有文字L2,且L1与L2 互补,从C1,C2中分别删除L1,L2,再将剩 余部分析取起来,构成的新子句C12称为C1与 C2的归结式(消解式),C1,C2称为C12的亲 本子句
定义４、设L是一个文字，则称L与L为互补 文字。 定义５、设C1、C2是命题逻辑中的两个子句， C1 中有文字L1 ， C２ 中有文字L２，且L1与L２ 互补， 从C1，C２中分别删除L1 ， L２，再将剩 余部分析取起来，构成的新子句C1２称为C1与 C2的归结式（消解式）， C1，C2称为C1２的亲 本子句
定理2、归结式C12是其亲本子句C1与C2 的逻辑结论 ※推论、设C1,C2是子句集S的两个子句, C12是它们的归结式,则 (1)若用C12代替C1和C2后得到新子 句集S1,则由S1的不可满足性可推出原 子句集S的不可满足性。即 S1不可满足→S不可满足
定理２、归结式C1２是其亲本子句C1与C2 的逻辑结论。 推论、设C1，C2是子句集S的两个子句， C1２是它们的归结式，则 （１）若用C1２代替C1和C2后得到新子 句集S1，则由S1的不可满足性可推出原 子句集S的不可满足性。即 S1不可满足S不可满足
(2)若把C12加入到S中,得到新子句集 S2,则S2与S在不可满足意义上是等价 的。即 S2不可满足◇S不可满足 例、用归结原理证明R是P,(P∧Q) →R,(SVU)→R,U的逻辑结 果
（２）若把C1２加入到S中，得到新子句集 S２，则S２与S在不可满足意义上是等价 的。即 S2不可满足 S不可满足 例、用归结原理证明R是P， （P Q） → R， （ SU） → R，U的逻辑结 果
3.2.3替换与合 定义6、一个替换( Substitution是形如{t1/x1 t2/x2…,n/xn}的有限集合,其中t,t2,…,tn 是项,x1,x2,,xn是互不相同的个体变元。 七/x表示用t代换x1。t与x不同,x也不能出 现在中(=1,2,n 例、(ax,g(y)y,fg(b)/z}是一个替换, g(y)x,fx)y}不是一个替换
3.2.3 替换与合一 定义６、一个替换(Substitution)是形如{t1 / x1 , t2 / x2 ,…,tn / xn }的有限集合，其中t1 , t2 ,…,tn 是项， x1 , x2 ,…,xn是互不相同的个体变元。 t i / xi表示用t i代换xi 。 t i与xi不同，xi也不能出 现在t j中(j=1,2,…,n)。 例、｛a/x, g(y)/y, f(g(b))/z}是一个替换， {g(y)/x, f(x)/y}不是一个替换