人工智能讲义AI05

第五章消解反演系统§5.1消解反演正向消解演绎系统的缺点什么是消解反演将结论取反加入前提条件再进行消解推理,其目标是产生一个空子句NIL.空子句表示有矛盾.因为只有在子句集中出现P和~P形式的母体子句对时,才会产生消解式NIL.消解反演有效性的证明将结论取反加到前提条件中推出矛盾,即证明前提和结论的否定不可能同时成立.设前提公式集为S,结论公式为W S

(~W)~(~(S(~W))) ~(~SV(~(~W))) ~(~SVW) ~(SW) 所以若S(~W)推出矛盾,即S(~W)永假,则SW永真.消解反演的优点目标明确,简单易行.消解反演系统的基本算法RESOLUTION将前提公式集S和结论公式W的否定~W化为子句集S0untilNILS0

或没有可消解的子句对do

Begin在S0中选取可消解的子句对Ci和Cj计算Ci和Cj的消解式Rij把Rij加入到S0中end举例例一每个储蓄钱的人都要获得利息.请证明:如果没有利息,那么就没有人去储蓄钱.证明:令S(x,y)表示“x储蓄y” M(x)表示“x是钱” I(x)表示“x是利息” E(x,y)表示“x要获得y” S:(x)((

y)(S(x,y)

M(y))

(

z)(I(z)

E(x,z)))W:~(

x)I(x)

(y)(z)(~(S(y,z)

M(z)))1把前提化为子句形(x)(~(

y)(S(x,y)

M(y))V(

z)(I(z)

E(x,z)))

(

x)((y)~(S(x,y)

M(y))V(

z)(I(z)

E(x,z)))(x)((y)(~S(x,y)V~M(y))V(

z)(I(z)

E(x,z)))令z=f(x)为Skolem函数:

(

x)((y)(~S(x,y)V~M(y))V(I(f(x))

E(x,f(x))))(x)(y)(~S(x,y)V~M(y)VI(f(x)))

(~S(x,y)V~M(y))V

E(x,f(x)))得到下列子句:(1)~S(x,y)V~M(y)VI(f(x))(2)~S(x,y)V~M(y))V

E(x,f(x))2结论的否定

~(~(

x)I(x)

(y)(z)(~(S(y,z)

M(z))))

化为子句形

~((

x)I(x)V(y)(z)(~(S(y,z)

M(z))))

~(

x)I(x)~(y)(z)(~(S(y,z)

M(z)))

(x)(~I(x))

(

y)(~(z)(~(S(y,z)

M(z))))(x)(~I(x))

(

y)(

z)(S(y,z)

M(z))

(x)(~I(x))

S(A,B)

M(B)得到下列子句:(3)~I(z) (4)S(A,B) (5)M(B)3消解~S(x,y)V~M(y)VI(f(x))~I(z)S(A,B)M(B)~S(x,y)V~M(y)~M(B)NIL{f(x)/z}{A/x,B/y}§5.2消解反演系统的控制策略引言例已知:任何能够阅读者都是识字的.海豚不识字但某些海豚是有智力的.求证:某些有智力者不能阅读.证:令R(x)表示x能阅读,L(x)表示x识字, D(x)表示x是海豚,I(x)表示x有智能.前提:(1)(x)(R(x)

L(x)) (2)(x)(D(x)~L(x)) (3)(

x)(D(x)

I(x)) 结论:(4)(

x)(I(x)~R(x))将结论取反后加入前提谓词公式集并化为子句集: (1)~R(x)VL(x) (2)~D(y)V~L(y) (3)D(A),I(A) (4)~I(z)VR(z) I(A)~I(z)VR(z)~R(x)VL(x)~D(y)V~L(y)D(A)R(A)L(A)~L(A)~I(z)VL(z)~R(y)V~D(y)~I(z)V~D(z)~D(A)~R(A)~I(A)NIL~D(A)~I(A)讨论对所有可消解的子句对进行消解对应于反演图的宽度优先搜索.子句集:S,(S),²(S),…迅速增大,系统效率很低.高效比完备更重要.简化字句集阅读PP85~87P86“2.归类消去”:如果有一个子句L中含有的文字组成的集合为{Li},而另一子句N中含有的文字组成的集合为{Nj}

则说子句L可以归类子句N文字优先消解法在当前子句集的能消解的子句对中,选其中有一个是文字的优先进行消解.前例采用文字优先消解法的消解过程:•讨论

为什么可以删除重言式?

归类消去的依据是什么?

P(A)为什么不能归类P(x)?T

{S}

{S}P(x)(P(A)VR(y)VS(z))P(x)I(A)~I(z)VR(z)~R(x)VL(x)~D(y)V~L(y)D(A)R(A)L(A)~L(A)~D(A)NILNIL支持集优先消解法支持集:目标公式取反后化成的子句和祖先中有这些子句的消解式所构成的子句集.支持集优先消解法:母体子句对中至少有一个子句在支持集中时才进行消解.逆向推理与反演前例采用支持集优先消解法的消解过程:I(A)~I(z)VR(z)~R(x)VL(x)~D(y)V~L(y)D(A)R(A)L(A)~I(z)VL(z)~I(z)V~D(z)~D(A)~I(A)NIL~D(A)~D(A)NILNILNILL(A)锁消解法配锁与锁合并对子句集中所出现的每一个文字(不论是否相同)都加以不同的编号,称为配锁.编号称为锁号. 如:C1=1P(x)V2Q(x)V3P(A)V4Q(A) C2=5~Q(y)V6P(A)V7W(y)在同一子句中经过置换出现相同的文字进行合一时,给该文字保留最小的锁号,称为锁合并. 如:S={A/x}则 C1•S=1P(A)V2Q(A)V3P(A)V4Q(A) =1P(A)V2Q(A) 锁消解当两子句中锁号最小的文字为互补文字时才进行消解,称为锁消解.如C1=1P(A)V2Q(x) C2=3~P(A)V4~Q(A) C3=6~P(A)V5~Q(A) C1和C2可进行锁消解得 2Q(x)V4~Q(A) C1和C3不可进行锁消解

举例:设初始子句集为 (1)1Q(B)V2P(u)

(2)3~P(w)V4Q(B)(3)5~W(v)V6~Q(v)(4)7W(v)V8~Q(B)1Q(B)V2P(u)7W(v)V8~Q(B)3~P(w)V4Q(B)5~W(v)V6~Q(v)6~Q(v)V8~Q(B)2P(u)4Q(B)NIL锁消解法的完备性虽然配锁是任意的,但是只要一个子句集是不可满足的,总可以找到能进行锁消解的子句对,直至出现空子句.即锁消解法是完备的.非形式的证明(反证法): 若一个子句集是不可满足的,而找不到可进行锁消解的子句对,即所有子句中最小锁号的文字均不互补,则只要把这些最小锁号的文字中的正文字取值为真,而把带“~”号的文字取值为假,则每个子句均为真,故子句集是可以满足的,与前提矛盾.

例:C1=1P(A)V2Q(x) C2=3P(A)V4~Q(x) C3=6~P(A)V5~Q(x) 所有子句中最小锁号的文字为: P(A),P(A),~Q(x). 只要取P(A)=T,Q(x)=F, 则 C1

C2

C3=T习题P100第4题P100第7题:“对于所有的x,y和z”P100第10题P100第3题P100第11题§5.3由消解反演求取答案的方法推定证明谓词演算不仅能用于定理证明,也能用于其他问题求解.例如,从前提公式集S出发,要证明结论(

x)W(x),是一个一般的谓词演算证明问题,而如果要推出是哪一个x能满足W(x),即要产生满足条件的变量x的实例,则是一个推定证明的问题.简例:已知无论约翰(John)在哪里,菲多(Fido)也在那里;现在约翰在学校,请问菲多在哪里?从给定的条件出发来推出某个事实,称为推定证明.答案求取过程

消解反演法的启示先证明从S能得到(

x)W(x)的结论.将结论与结论的否定构成的重言式与前提条件一起组成初始公式集参加消解.消解的过程仿照证明的消解反演过程进行,消解结束后会留下结论的有关部分,即为答案,其中的变量已被进行必要的置换(例化).简例的求解前提:(x)(AT(JOHN,x)AT(FIDO,x)) AT(JOHN,SCHOOL)先证:(x)AT(FIDO,x)化成子句,消解反演:~AT(FIDO,x)~AT(JOHN,y)VAT(FIDO,y)~AT(JOHN,x)AT(JOHN,SCHOOL)NIL{x/y}{SCHOOL/x}“菲多在哪里?”的消解反演树~AT(FIDO,x)VAT(FIDO,x)~AT(JOHN,y)VAT(FIDO,y)AT(FIDO,x)V~AT(JOHN,x)AT(JOHN,SCHOOL)AT(FIDO,SCHOOL){x/y}{SCHOOL/x}“菲多在哪里?”的修改证明树要么菲多不在任何地方,要么菲多在某个地方.通过消解反演求取问题答案的步骤(1)先把要求解的问题变成相应的证明问题,得到一棵消解反演树;(2)把目标公式的否定产生的每个子句再加以否定,加入到原子句中构成重言式,并与原前提条件子句组成新的初始子句集;(3)从新的初始子句集开始,执行和反演树一样的消解,在对应于反演树根部空子句处得到的子句即为问题的一个答案,消解所产生的树称为修改证明树.举例(PP94-96)前提公式子句集：~A(x)VF(x)VG(f(A))x不是大学生Vx听计算机课VA的兄弟是研究生~F(y)VB(y)y听计算机课y懂外语~F(z)VC(z)z听计算机课z懂计算机~G(x1)VB(x1)x1是研究生x1懂外语~G(y1)VD(y1)y1是研究生y1会写论文A(E)VF(h(z1))E是大学生Vz1的学生听计算机课(z1为计算机系的老师)谁既懂外语又懂计算机或既会写论文又懂外语？目标公式：(x)((B(x)C(x))V(D(x)B(x)))目标公式取反后化为子句：~B(x2)V~C(x2)~D(y2)V~B(y2)答案：(B(E)C(E))V(D(f(A))B(f(A)))V(B(h(z1))C(h(z1)))E既懂外语又懂计算机；A的兄弟既会写论文又懂外语；z1（计算机系老师）的学生既懂外语又懂计算机。含有全称量词的目标公式的答案提取目标公式子句中的Skolem函数当目标公式含有全称量词时,在目标公式的否定式中就会出现存在量词,把公式变成子句就要引入Skolem函数,在提取回答时,应正确解释这些Skolem函数的意义.例1 前提:每个人都是某人的孩子. (

x)(y)C(x,y)

如果x是y的孩子,那么y是x的父辈. (

x)(

y)[C(x,y)P(y,x)]

问题:对于任意一个x,谁是他的父辈? 目标:对于任一个x,存在y是他的父辈. (

x)(y)P(y,x)前提子句:(1)C(x,f(x)) (2)~C(x,y)VP(y,x)目标公式的否定化为子句: ~(

x)(y)P(y,x)

不是所有的x都有父辈

(

x)(

y)~P(y,x) 存在x没有父辈 (3)~P(y,A)消解反演树:~P(y,A)~C(x,y)VP(y,x)~C(A,y)C(x,f(x))NIL修改证明树:~P(y,A)VP(y,A)~C(x,y)VP(y,x)~C(A,y)VP(y,A)C(x,f(x))P(f(A),A)

Skolem函数A在这里的意义是,对任何一个人A,我们都能证明P(f(A),A),即A总有一个父辈f(A).因此,在修改证明树中可以把目标公式子句中出现的Skolem函数换成新的变量,如t.这样得到的回答语句为P(f(t),t),意义更为明了,即任一个人t的父辈是f(t).要么有某人无父辈,要么任一人都有父辈例2前提:或者是B叫所有的人自己投自己的票,或者 是A叫所有的人自己投自己的票. (w)P(B,w,w)V(

u)P(A,u,u)

问题:谁在叫所有的人投什么人的票?目标:存在一个人叫所有的人投某人的票. (x)(y)(

z)P(x,y,z)

前提子句:P(B,w,w)VP(A,u,u)

目标的否定化为子句: ~(x)(y)(

z)P(x,y,z)

(x)(

y)(z)~P(x,y,z) ~P(x,g(x),z)消解反演树~P(x,g(x),z)P(B,w,w)VP(A,u,u)P(B,w,w)NIL{A/x,g(A)/u,g(A)/z}{B/x,g(B)/w,g(B)/z}修改证明树~P(x,t,z)VP(x,t,z)P(B,w,w)VP(A,u,u)P(B,w,w)VP(A,t,t){A/x,t/u,t/z}P(A,t,t)VP(B,t,t){B/x,t/w,t/z}比较答案与目标的形式可知问题有两个答案，两文字受不同的全称量词约束答案求取过程的步骤首先按某种消解策略寻找一个消解反演树,并记下每一步消去的文字;将由目标公式的否定式求得的子句中的Skolem函数以新的变量代替;把由目标公式的否定的到的子句与子句的否定式构成重言式;仿照原始反演树的结构生成一棵修改证明树,在修改证明树中每次所消去的文字是由反演树中相应的消解决定的;修改证明树树根上的子句就是所求取的回答语句.§5.4Horn子句逻辑一般子句与Horn子句(P97)Horn子句的逻辑程序(PP97~99)Horn子句逻辑程序运行的实质过程与事实目标口Horn子句与Prolog逻辑程序设计语言:-sister(x,Edward),parents(y,z,Edward)sister(x,y):-female(x),parents(y,u,v),parents(x,u,v):-female(x),parents(Edward,u,v),parents(x,u,v)),parents(y,z,Edward)Female(Sdifen):-:-parents(Edward,u,v),parents(Alice,u,v)),parents(y,z,Edward)Parents(Edward,Victoria,Albert):-:-parents(Sdifen,Victoria,Albert),parents(y,z,Edward)Female(Alice):-:-parents(Edward,u,v),parents(Sdifen,u,v)),parents(y,z,Edward)⑩①⑦②:-parents(Edward,u,v),parents(Alice,u,v)),parents(y,z,Edward):-parents(Alice,Victoria,Albert),parents(y,z,Edward)parents(Alice,Victoria,Albert):-Parents(