人工智能第3章謂詞演算與歸結(jié)原理.ppt

《人工智能第3章謂詞演算與歸結(jié)原理.ppt》由會(huì)員分享，可在線閱讀，更多相關(guān)《人工智能第3章謂詞演算與歸結(jié)原理.ppt（59頁(yè)珍藏版）》請(qǐng)?jiān)谘b配圖網(wǎng)上搜索。

第三章謂詞演算與歸結(jié)原理,一階謂詞演算是一種形式語言，具有嚴(yán)密的理論體系是一種常用的知識(shí)表示方法例：City（北京）City（上海）Age（張三，23）(?x)(?y)(?z)(F(x,y)?F(y,z)?GF(x,z)),3.1歸結(jié)原理,歸結(jié)原理是一種定理證明方法，1965年由Robinson提出，從理論上解決了定理證明問題。子句集無量詞約束元素只是文字的析取否定符只作用于單個(gè)文字元素間默認(rèn)為合取例：{~I(z)?R(z),I(A),~R(x)?L(x),~D(y)},化子句集的方法,例：(?z)(?x)(?y){[(P(x)?Q(x))?R(y)]?U(z)}1,消蘊(yùn)涵符理論根據(jù)：a?b=>~a?b(?z)(?x)(?y){[~(P(x)?Q(x))?R(y)]?U(z)}2,移動(dòng)否定符理論根據(jù)：~(a?b)=>~a?~b~(a?b)=>~a?~b~(?x)P(x)=>(?x)~P(x)~(?x)P(x)=>(?x)~P(x)(?z)(?x)(?y){[(~P(x)?~Q(x))?R(y)]?U(z)},化子句集的方法（續(xù)1）,3,變量標(biāo)準(zhǔn)化即：對(duì)于不同的約束，對(duì)應(yīng)于不同的變量(?x)A(x)?(?x)B(x)=>(?x)A(x)?(?y)B(y)4,量詞左移(?x)A(x)?(?y)B(y)=>(?x)(?y){A(x)?B(y)}5,消存在量詞(skolem化）原則：對(duì)于一個(gè)受存在量詞約束的變量，如果他不受全程量詞約束，則該變量用一個(gè)常量代替，如果他受全程量詞約束，則該變量用一個(gè)函數(shù)代替。(?z)(?x)(?y){[(~P(x)?~Q(x))?R(y)]?U(z)}=>(?x){[(~P(x)?~Q(x))?R(f(x))]?U(a)},化子句集的方法（續(xù)2）,6,化為合取范式即(a?b)?(c?d)?(e?f)的形式(?x){[(~P(x)?~Q(x))?R(f(x))]?U(a)}=>(?x){(~P(x)?~Q(x))?R(f(x))?U(a)}=>(?x){[~P(x)?R(f(x))?U(a)]?[~Q(x))?R(f(x))?U(a)]}7,隱去全稱量詞{[~P(x)?R(f(x))?U(a)]?[~Q(x))?R(f(x))?U(a)]},化子句集的方法（續(xù)3）,8,表示為子句集{~P(x)?R(f(x))?U(a),~Q(x))?R(f(x))?U(a)}9,變量標(biāo)準(zhǔn)化（變量換名）{~P(x1)?R(f(x1))?U(a),~Q(x2))?R(f(x2))?U(a)},定理：若S是合式公式F的子句集，則F永假的充要條件是S不可滿足。S不可滿足：若nil?S，則S不可滿足。證明的思路：目標(biāo)的否定連同已知條件一起，化為子句集，并給出一種變換的方法，使得S?S1?S2?...?Sn同時(shí)保證當(dāng)Sn不可滿足時(shí)，有S不可滿足。,3.2歸結(jié)方法（命題邏輯）,設(shè)子句：C1=L?C1’C2=(~L)?C2’則歸結(jié)式C為：C=C1’?C2’定理：子句集S={C1,C2,…,Cn}與子句集S1={C,C1,C2,…,Cn}的不可滿足性是等價(jià)的。其中，C是C1和C2的歸結(jié)式。,歸結(jié)的例子,設(shè)公理集：P,(P?Q)?R,(S?T)?Q,T求證：R子句集：(1)P(2)~P?~Q?R(3)~S?Q(4)~T?Q(5)T(6)~R（目標(biāo)求反）,化子句集：(P?Q)?R=>~(P?Q)?R=>~P?~Q?R(S?T)?Q=>~(S?T)?Q=>(~S?~T)?Q=>(~S?Q)?(~T?Q)=>{~S?Q,~T?Q},子句集：(1)P(2)~P?~Q?R(3)~S?Q(4)~T?Q(5)T(6)~R（目標(biāo)求反）,歸結(jié)：(7)~P?~Q(2,6)(8)~Q(1,7)(9)~T(4,8)(10)nil(5,9),3.3謂詞邏輯的歸結(jié)原理,問題：如何找歸結(jié)對(duì)例：P(x)?Q(y),~P(f(y))?R(y)P(A)?Q(y),~P(f(y))?R(y)基本概念置換s={t1/v1,t2/v2,…,tn/vn}對(duì)公式E實(shí)施置換s后得到的公式稱為E的例，記作Es。例：s1={z/x,Ay},則：P[x,f(y),B]s=P[z,f(A),B],合一如果存在一個(gè)S置換，使得{Ei}中E1s=E2s=E3s=…=Ens，則稱{Ei}是可合一的。S為{Ei}的合一者。例：{P(x,f(y),B),P(z,f(B),B)}置換s={A/x,B/y,A/z}是一個(gè)合一者,因?yàn)椋篜(x,f(y),B)s=P(A,f(B),B)P(z,f(B),B)s=P(A,f(B),B)置換s={z/x,B/y}和置換s={x/z,B/y}也都是合一者。結(jié)論：合一者不唯一。,最一般合一者（mgu）置換最少，限制最少，產(chǎn)生的例最具一般性。如前面的例子：{P(x,f(y),B),P(z,f(B),B)}對(duì)于置換{A/x,B/y,A/z}，產(chǎn)生的例是：P(A,f(B),B)對(duì)于置換={z/x,B/y}，產(chǎn)生的例是：P(z,f(B),B)mgu也不是唯一的。,合一算法遞歸過程UNIFY(E1,E2)1ifE1或E2是一個(gè)原子，交換E1和E2的位置，使E1是一個(gè)原子，do2beginIfＥ1和Ｅ2是相同的，returnNILIfE1是一個(gè)變量，doBeginIfE1出現(xiàn)在E2中，returnFAILreturn{E2/E1}endIfE2是一個(gè)變量，return{E1/E2}returnFAILEnd,F1?E1的第一個(gè)元素，T1?E1的其余元素F2?E2的第一個(gè)元素，T2?E2的其余元素Z1?UNIFY(F1,F2)IfZ1=FAIL,returnFAILG1?Z1作用到T1的結(jié)果G２?Z2作用到T2的結(jié)果Z2?UNIFY(G1,G2)IfZ2=FAIL,returnFAILReturnZ1和Z2的合成,合一算法,例：{P(x,x,z),P(f(y),f(B),y)}前綴表示：(Pxxz)(P(fy)(fB)y)置換：{(fy)/x}(P(fy)(fy)z)(P(fy)(fB)y)置換：{B/y},并使得{(fB)/x}(P(fB)(fB)z)(P(fB)(fB)B)置換：{B/z}得到置換：{(fB)/x，B/y，B/z}置換后的結(jié)果：(P(fB)(fB)B),歸結(jié)舉例,設(shè)公理集：(1)Whoevercanreadisliterate(?x)(R(x)?L(x))(2)Dolphinsarenotliterate(?x)(D(x)?~L(x))(3)Somedolphinsareintelligent(?x)(D(x)?I(x))求證:(4)Somewhoareintelligentcannotread(?x)(I(x)?~R(x)),化子句集：(?x)(R(x)?L(x))=>(?x)(~R(x)?L(x))=>~R(x)?L(x)(1)(?x)(D(x)?~L(x))=>(?x)(~D(x)?~L(x))=>~D(x)?~L(x)(2)(?x)(D(x)?I(x))=>D(A)?I(A)=>D(A)(3)I(A)(4),目標(biāo)求反：~(?x)(I(x)?~R(x))=>(?x)~(I(x)?~R(x))=>(?x)(~I(x)?R(x))=>~I(x)?R(x)(5)換名后得字句集：~R(x1)?L(x1)~D(x2)?~L(x2)D(A)I(A)~I(x5)?R(x5),例題的歸結(jié)樹,~R(x1)?L(x1)~D(x2)?~L(x2)D(A)I(A)~I(x5)?R(x5),I(A),~I(x5)?R(x5),,,R(A),{A/x5},~R(x1)?L(x1),,,L(A),{A/x1},~D(x2)?~L(x2),,,~D(A),{A/x2},D(A),,,nil,單元優(yōu)先策略,歸結(jié)反演的產(chǎn)生式系統(tǒng),把不斷進(jìn)行歸結(jié)的反演系統(tǒng)認(rèn)為是一個(gè)產(chǎn)生式系統(tǒng)．綜合數(shù)據(jù)庫(kù)是子句集規(guī)則表就是歸結(jié)生式系統(tǒng)的基本算RESOLUTI0N1．CLAUSES：=S；S為初始的基本子句集2．UntilNIL是CLAUSES的元素，do3．Begin4.在CLAUSES中選兩個(gè)不同的可歸結(jié)的子句Ci、Cj5.計(jì)算Ci、Cj的歸結(jié)式rij6.附加rij到CLAUSES所產(chǎn)生的集end,謂詞邏輯的歸結(jié)方法,對(duì)于子句C1?L1和C2?L2，如果L1與~L2可合一，且s是其合一者，則(C1?C2)s是其歸結(jié)式。例：P(x)?Q(y),~P(f(z))?R(z)=>Q(y)?R(z),歸結(jié)方法的控制策略,寬度優(yōu)先策略支持集策略單元優(yōu)先策略單元子句優(yōu)先策賂線性輸入形策略,,,,原始子句集S,第三級(jí)歸結(jié)式,第二級(jí)歸結(jié)式,第一級(jí)歸結(jié)式,I(A),~I(z)∨R(z),~R(x)∨L(x),~D(y)∨~L(y),D(A),R(A),L(A),,,~I(z)∨L(z),~R(y)∨~D(y),~L(A),,,,,D(A),L(A),~I(z)∨~D(z),~I(z)∨~D(z),~R(A),~I(A),,,,,,,,,,,,,,,,,,NIL,…,…,,,寬度優(yōu)先搜索過程,,,,I(A),~I(z)∨R(z),~R(x)∨L(x),~D(y)∨~L(y),D(A),原始子句集S,第三級(jí)歸結(jié)式,第二級(jí)歸結(jié)式,第一級(jí)歸結(jié)式,R(A),L(A),,,~I(z)∨L(z),,~I(y)∨~D(y),,,,,,~D(A),,L(A),,,~I(A),~D(A),~D(A),,,,,,,,,支持集策略搜索過程,,,,I(A),~I(z)∨R(z),~R(x)∨L(x),~D(y)∨~L(y),D(A),原始子句集S,第三級(jí)歸結(jié)式,第二級(jí)歸結(jié)式,第一級(jí)歸結(jié)式,R(A),L(A),,,~I(z)∨L(z),~R(y)∨~D(y),~L(A),,,,,L(A),~I(z)∨~D(z),~I(y)∨~D(y),~R(A),,,,,,,,,,,,,…,,~I(A),,,…,線性輸入形策略搜索過程,~Q(x)∨~P(x),Q(y)∨~P(y),~Q(w)∨P(w),~Q(w),Q(u)∨P(A),P(A),NIL,,,,,,,,,,祖先過濾策略的搜索過程,3.4基于歸結(jié)的問答系統(tǒng),例：已知：IfFidogoeswhereverJohngoesandifJohnisatschool,whereisFido?(?x)[AT(John,x)?AT(Fido,x)]AT(John,School)求證：(?x)AT(Fido,x)子句集：~AT(John,x1)?AT(Fido,x1)AT(John,School)~AT(Fido,x2),~AT(Fido,x2),~AT(John,x1)?AT(Fido,x1),子句集：~AT(John,x1)?AT(Fido,x1)AT(John,School)~AT(Fido,x2),{x2/x1},AT(John,School),{School/x2},AT(Fido,x2)?,?AT(Fido,x2),AT(Fido,School),提取回答的過程,先進(jìn)行歸結(jié)，證明結(jié)論的正確性；用重言式代替結(jié)論求反得到的子句；按照證明過程，進(jìn)行歸結(jié)；最后，在原來為空的地方，得到的就是提取的回答。修改后的證明樹稱為修改證明樹,例：猴子摘香蕉問題,,,問題的表示,已知：1,~ON(s0)2,(?x)(?s)(~ON(s)?AT(box,x,push(x,s)))3,(?s)(ON(climb(s)))4,(?s)((ON(s)?AT(box,c,s))?HB(grasp(s)))5,(?x)(?s)(AT(box,x,s)?AT(box,x,climb(s)))求解：(?s)HB(s),問題的子句集,1,~ON(s0)2,ON(s1)?AT(box,x1,push(x1,s1))3,ON(climb(s2))4,~ON(s3)?~AT(box,c,s3)?HB(grasp(s3))5,~AT(box,x4,s4)?AT(box,x4,climb(s4))6,~HB(s5),返回,~HB(s5),~ON(s3)?~AT(box,c,s3)?HB(grasp(s3)),,,,~ON(s3)?~AT(box,c,s3),{grasp(s3)/s5},,,ON(climb(s2)),,,{climb(s2)/s3},~AT(box,c,climb(s2)),,,~ON(s0),,ON(s1)?AT(box,x1,push(x1,s1)),,{s0/s1},AT(box,x1,push(x1,s0)),,,,~AT(box,x4,s4)?AT(box,x4,climb(s4)),{x4/x1,push(x4,s0)/s4},,AT(box,x4,climb(push(x4,s0))),,,,,NIL,{c/x4,push(c,s0)/s2},,,HB(s5)?,HB(grasp(s3))?,?HB(grasp(climb(s2))),HB(grasp(climb(push(c,s0)))),歸結(jié)方法小結(jié),求子句集，進(jìn)行歸結(jié)，方法簡(jiǎn)單通過修改證明樹的方法，提取回答方法通用求解效率低，不宜引入啟發(fā)信息不宜理解推理過程,3.5基于規(guī)則的正向演繹系統(tǒng),問題：歸結(jié)方法不自然可能會(huì)丟失蘊(yùn)涵關(guān)系中所包含的控制信息例：以下蘊(yùn)涵式：~A?~B?C~C?A?B~A?~C?B~A?C?B~B?~C?A~B?A?C均與子句(A?B?C)等價(jià)，但顯然上面的蘊(yùn)涵式信息更豐富。,事實(shí)表達(dá)式的與或形及其表達(dá),與或形無量詞約束否定符只作用于單個(gè)文字只有“與”、“或”例：(?u)(?v)(Q(v,u)?~((R(v)?P(v))?S(u,v)))=>(?u)(?v)(Q(v,u)?((~R(v)?~P(v))?~S(u,v)))=>Q(v,A)?((~R(v)?~P(v))?~S(A,v))Skolem化=>Q(w,A)?((~R(v)?~P(v))?~S(A,v))主合取元變量換名,事實(shí)的與或樹表示,例：Q(w,A)?((~R(v)?~P(v))?~S(A,v)),Q(w,A)?((~R(v)?~P(v))?~S(A,v)),Q(w,A),(~R(v)?~P(v))?~S(A,v),~R(v)?~P(v),~S(A,v),~R(v),~P(v),,,,,,,,解圖集：Q(w,A),~R(v)?~S(A,v),~P(v)?~S(A,v),應(yīng)用規(guī)則對(duì)與或圖作變換,對(duì)規(guī)則的形式：L?W其中，L是單文字，W是與或形，變量受全稱量詞約束例：(?x)(((?y)(?z)P(x,y,z))?(?u)Q(x,u))=>(?x)(~((?y)(?z)P(x,y,z))?(?u)Q(x,u))=>(?x)((?y)(?z)~P(x,y,z)?(?u)Q(x,u))=>(?x)(?y)(?z)(?u)(~P(x,y,z)?Q(x,u))=>~P(x,y,f(x,y))?Q(x,u)=>P(x,y,f(x,y))?Q(x,u)=>P(x1,y1,f(x1,y1))?Q(x1,u1)換名例：(L1?L2)?W=>L1?W和L2?W,命題邏輯的情況,例：事實(shí)：((P?Q)?R)?(S?(T?U))規(guī)則：S?(X?Y)?Z,((P?Q)?R)?(S?(T?U)),(P?Q)?R,S?(T?U),,,,P?Q,R,,,S,T?U,,,P,Q,,,,T,U,,,,S,,X?Y,Z,,,,X,Y,,,P?Q?SP?Q?T?US?RR?T?UP?Q?X?ZP?Q?Y?ZR?X?ZR?Y?Z,規(guī)則的子句：S?(X?Y)?Z=>~S?(X?Y)?Z=>~S?X?Z~S?Y?Z,結(jié)論：加入規(guī)則后得到的解圖，是事實(shí)與規(guī)則對(duì)應(yīng)子句的歸結(jié)式,例：事實(shí)：A?B規(guī)則集：A?C?DB?E?G目標(biāo)公式：C?G,A?B,A,B,,,,A,,C,D,,,B,,E,G,,,,C,,G,,目標(biāo),謂詞邏輯的情況,事實(shí)表達(dá)式化成與或形規(guī)則化成L?W的形式，其中L為單文字目標(biāo)用Skolem化的對(duì)偶形式，即消去全稱量詞，用Skolem函數(shù)代替保留存在量詞對(duì)析取元作變量換名例：(?y)(?x)(P(x,y)?Q(x,y))=>(?y)(P(f(y),y)?Q(f(y),y))=>P(f(y1),y1)?Q(f(y2),y2)換名規(guī)則每使用一次，都要進(jìn)行一次換名,例：事實(shí)：P(x,y)?(Q(x,A)?R(B,y))規(guī)則集：P(A,B)?(S(A)?X(B))Q(B,A)?U(A)R(B,B)?V(B)目標(biāo)：S(A)?X(B)?U(A)?V(B),P(x,y)?(Q(x,A)?R(B,y)),P(x,y),Q(x,A)?R(B,y),,,,Q(x,A),R(B,y),,,,P(A,B),{A/x,B/y},S(A),X(B),,,,,Q(B,A),{B/x},U(A),,,R(B,B),{B/y},V(B),,一致解圖,如果一個(gè)解圖中所涉及的置換是一致的，則該解圖稱為一致解圖。設(shè)有置換集{u1,u2,…,un},其中:ui={ti1/vi1,…,tin/vin}，定義表達(dá)式：U1=(v1,1,…,v1,m1,…,vn,1,…,vn,mn)U2=(t1,1,…,t1,m1,…,tn,1,…,tn,mn)置換集{u1,u2,…,un}稱為一致的，當(dāng)且僅當(dāng)U1和U2是可合一的。U1、U2的mgu是{u1,u2,…,un}的合一復(fù)合。置換集的合一復(fù)合運(yùn)算是可結(jié)合和可交換的。,一致置換舉例,,舉例,事實(shí)：~D(F)?(B(F)?I(F))規(guī)則：R1:~D(x)?~T(x)R2:B(y)?N(y)目標(biāo)：~T(u)?N(v),~D(F)?(B(F)?I(F)),~D(F),B(F)?I(F),,,,B(F),I(F),,,,~D(x),{F/x},~T(F),,R1,~T(u),{F/u},B(y),,{F/y},N(F),,R2,N(v),,,{F/v},目標(biāo),目標(biāo),U1=(x,u,y,v)U2=(F,F,F,F)合一復(fù)合u：{F/x,F/u,F/y,F/v}作用于目標(biāo)：[~T(u)?N(v)]u=~T(F)?N(F),規(guī)則：R1:~D(x)?~T(x)R2:B(y)?N(y)目標(biāo)：~T(u)?N(v),正向演繹系統(tǒng)小結(jié),事實(shí)表達(dá)式為與或形規(guī)則形式：L?W,其中L為單文字目標(biāo)公式為文字析取對(duì)事實(shí)和規(guī)則進(jìn)行Skolem化，消去存在量詞，變量受全稱量詞約束，對(duì)主合取元和規(guī)則中的變量換名用“對(duì)偶形”對(duì)目標(biāo)進(jìn)行Skolem化，消去全稱量詞，變量受存在量詞約束，對(duì)析取元中的變量換名事實(shí)表達(dá)成與或樹，其中，“?”對(duì)應(yīng)樹中“與”，“?”對(duì)應(yīng)樹中“或”從事實(shí)出發(fā)，正向應(yīng)用規(guī)則，到得到目標(biāo)節(jié)點(diǎn)為結(jié)束的一致解圖為止存在合一復(fù)合時(shí)，則解圖是一致的,3.6基于規(guī)則的逆向演繹系統(tǒng),目標(biāo)為任意形的表達(dá)式用“對(duì)偶形”對(duì)目標(biāo)進(jìn)行Skolem化，即消去全稱量詞，變量受存在量詞約束，對(duì)主析取元中的變量換名目標(biāo)用與或樹表示，其中，“?”對(duì)應(yīng)樹中“與”，“?”對(duì)應(yīng)樹中“或”事實(shí)表達(dá)式是文字的合?。ㄓ形鋈r(shí)可轉(zhuǎn)化為規(guī)則）規(guī)則形式：L?W,其中W為單文字，如形為：L?W1?W2，則變換為：L?W1和L?W2從目標(biāo)出發(fā)，逆向應(yīng)用規(guī)則，到得到事實(shí)節(jié)點(diǎn)為結(jié)束條件的一致解圖為止,例：事實(shí)：D(F)~B(F)W(F)M(N)規(guī)則：R1:(W(x1)?D(x1))?F(x1)R2:(F(x2)?~B(x2))?~A(y2,x2)R3:D(X3)?A(x3)R4:C(x4)?A(x4)R5:M(x5)?C(x5)目標(biāo)：C(x)?D(y)?~A(x,y),C(x)?D(y)?~A(x,y),C(x),D(y),~A(x,y),,,,,,C(x5),{x/x5},M(x),,R5,,M(N),{N/x},,D(F),{F/y},,~A(y2,x2),{x/y2,y/x2},F(y),~B(y),,,,R2,,~B(F),{F/y},,F(x1),{y/x1},W(y),D(y),,,,R1,,W(F),{F/y},,D(F),{F/y},一致性檢查,置換集{{x/x5},{N/x},{F/y},{x/y2,y/x2},{F/y},{y/x1},{F/y},{F/y}}U1=(x5,x,y,y2,x2,y,x1,y,y)U2=(x,N,F,x,y,F,y,F,F)合一復(fù)合{N/x5,N/x,F/y,N/y2,F/x2,F/x1}目標(biāo)得到的解答C(x)?D(y)?~A(x,y)=>C(N)?D(F)?~A(N,F),Horn子句與PROLOG,Horn子句是一類特殊的子句，體現(xiàn)為下列三種形式：規(guī)則：前項(xiàng)是正文字的合取，后項(xiàng)是單個(gè)正文字事實(shí)：當(dāng)前項(xiàng)為空時(shí)，表示事實(shí)目標(biāo)：當(dāng)后項(xiàng)為空時(shí)，表示目標(biāo)Horn子句構(gòu)成了PROLOG語言的基礎(chǔ),在PROLOG中的表示,規(guī)則：Pn:-Pn1,Pn2,…,Pnm含義：Pn1^Pn2^…^Pnm?Pn事實(shí)：Pi:-目標(biāo)：:-Pj1,Pj2,…,Pjk,PROLOG,增加了“否定”，但不是真正意義下的否定在規(guī)則前項(xiàng)中可以使用“或”，只是為了書寫更方便。采用回溯式搜索策略PROLOG實(shí)際是一個(gè)基于規(guī)則的逆向系統(tǒng),舉例,1,On(a,b):-2,On(b,c):-3,Above(X3,Y3):-On(X3,Y3)4,Above(X4,Y4):-On(X4,Z4),Above(Z4,Y4)目標(biāo)：:-Above(A,C),1,On(A,B):-2,On(B,C):-3,Above(x3,y3):-On(x3,y3)4,Above(x4,y4):-On(x4,z4),Above(z4,y4):-Above(A,C),Above(A,C),Above(x3,y3),,On(A,C),,{A/x3,C/y3},R3,無匹配,Above(x4,y4),,On(A,z4),Above(z4,C),{A/x4,C/y4},,,,R4,On(A,B),,{B/z4},事實(shí)1,B/z4,Above(x3’,y3’),,{B/x3’,C/y3’},On(B,C),,事實(shí)2,R3,3.7一些深入的問題,修剪不一致的局部解圖建立規(guī)則連接圖結(jié)構(gòu)規(guī)則的多次調(diào)用規(guī)則的遞歸調(diào)用加快匹配的速度,3.8正、逆向系統(tǒng)對(duì)比,事實(shí)表達(dá)式任意形規(guī)則形式：?jiǎn)挝淖?W目標(biāo)公式為文字析取對(duì)事實(shí)、規(guī)則消存在量詞，Skolem化用對(duì)偶形消目標(biāo)的全稱量詞，Skolem化事實(shí)表達(dá)式與或樹，“?”對(duì)“與”，“?”對(duì)應(yīng)“或”從事實(shí)出發(fā)，正向應(yīng)用規(guī)則以目標(biāo)為結(jié)束的一致解圖,事實(shí)表達(dá)式是合取形規(guī)則形式：L?單文字目標(biāo)公式任意形對(duì)事實(shí)、規(guī)則消存在量詞，Skolem化用對(duì)偶形消目標(biāo)的全稱量詞，Skolem化目標(biāo)公式的與或樹，“?”對(duì)“與”，“?”對(duì)應(yīng)“或”從目標(biāo)出發(fā)，逆向應(yīng)用規(guī)則以事實(shí)為結(jié)束的一致解圖,