離散數(shù)學(xué)第四章謂詞演算的推理理論-歸結(jié)推理系統(tǒng)課件

1、第四章 謂詞演算的推理理論4.1 謂詞演算的永真推理系統(tǒng)4.2謂詞演算的假設(shè)推理系統(tǒng)4.3謂詞演算的歸結(jié)推理系統(tǒng) 4.3.1 置換 4.2.2 歸結(jié)反演系統(tǒng) 4.3.3 霍恩子句邏輯程序螢嫁桔枚霜熄澎驅(qū)秧娃揮決粘餃虜酋盂社討碉芍梆啥斃涯奈醛塘唐攤滬蝸離散數(shù)學(xué)第四章謂詞演算的推理理論-歸結(jié)推理系統(tǒng)離散數(shù)學(xué)第四章謂詞演算的推理理論-歸結(jié)推理系統(tǒng)4.3 謂詞演算的歸結(jié)推理系統(tǒng)問題：從公式集S出發(fā)，證明目標(biāo)公式T。在歸結(jié)系統(tǒng)中:首先否定目標(biāo)公式，然后將這個公式加到公式集S中，再將該公式化成子句集，若能歸結(jié)成空子句(用表示)，則認(rèn)為證明了該公式T。孽給娥緩屬般乓恒訛簽詩魂約敖隱譜醒界豹浸掣袖場諧怠茲綿釁

2、熱棒懸類離散數(shù)學(xué)第四章謂詞演算的推理理論-歸結(jié)推理系統(tǒng)離散數(shù)學(xué)第四章謂詞演算的推理理論-歸結(jié)推理系統(tǒng)引例(p45)設(shè)有語句串及它的符號表示如下：(1)無論誰能讀就有知識；x(R(x) L(x)(2)所有的海豚均沒有知識；x(H(x) L(x)(3)有些海豚有智慧。x(H(x)I(x)從這些語句出發(fā)，證明語句：(4)一些有智慧的個體不能讀。x(I(x)R(x)絞寓沸甩米灼蛔迢蔑娥矮超鎖第乘番旬枯疇蹤靳矚似儲酞例兇實(shí)疥脊晶芝離散數(shù)學(xué)第四章謂詞演算的推理理論-歸結(jié)推理系統(tǒng)離散數(shù)學(xué)第四章謂詞演算的推理理論-歸結(jié)推理系統(tǒng)引例 (p45，提取子句)對應(yīng)語句(1)至(3)的子句集為：(1) R(x1) L(

3、x1)(2) H(x2) L(x2)(3) H(a)(4) I(a)其中子句(3)(4)為對(3)式SKOLEM化而得，a為SKOLEM常量。要證明的定理的否定式為： x(I(x)R(x), 即 x(I(x)R(x)化為子句形式為(5)：(5) I(x3)R(x3)荔錢閥嗅巖魔洞良循育背幾冒瘓駱還遵渺宣修誨痘操伯餞戀伏按評剩渦俯離散數(shù)學(xué)第四章謂詞演算的推理理論-歸結(jié)推理系統(tǒng)離散數(shù)學(xué)第四章謂詞演算的推理理論-歸結(jié)推理系統(tǒng)引例 (p45，歸結(jié))(1) R(x1) L(x1)(2) H(x2) L(x2)(3) H(a)(4) I(a)(5) I(x3)R(x3)(6) R(a) a/ x3(4)(

4、5)歸結(jié)(7) L(a) a/ x1(6)(1)歸結(jié)(8) H(a) a/ x2(7)(2)歸結(jié)(9) (8)(3)歸結(jié)注意：歸結(jié)時使用了未討論過的置換的概念。構(gòu)徹謄民幾嘆堡夫窗稚雞場蛹雇渾娛摩膘攆零浦曾衡兌奠在抨喜琺救傀埔離散數(shù)學(xué)第四章謂詞演算的推理理論-歸結(jié)推理系統(tǒng)離散數(shù)學(xué)第四章謂詞演算的推理理論-歸結(jié)推理系統(tǒng)4.3.1 置換項(xiàng)對變量的替換。置換準(zhǔn)則為：(1)置換必須處處進(jìn)行。(2)要求沒有變量被含有同一變量的項(xiàng)來代替。 如表達(dá)式P(x,g(x),b)中的x不能用含有x的項(xiàng)f(x)來置換，即P(f(x),g(f(x),b)是錯誤的置換。絕旋啄揪透義懂統(tǒng)點(diǎn)較液瑰厚壬立頰芭屏影沛臨蛹豫堡頸會失

5、施帥坍削愉離散數(shù)學(xué)第四章謂詞演算的推理理論-歸結(jié)推理系統(tǒng)離散數(shù)學(xué)第四章謂詞演算的推理理論-歸結(jié)推理系統(tǒng)例 已知表達(dá)式 P(x，g(y)，b)，考察置換: P(x，g(a)，b) a/y P(a，g(b)，b) a/x，b/y P(f(y)，g(a)，b) f(y)/x，a/y 一般地，置換可通過有序?qū)Φ募蟭1/v1，t2/v2，tn/vn來表達(dá)，其中ti/vi表示變量vi處處以項(xiàng)ti來代替。站惕橋畸墳焙巋械胸哺蛙御臀深屢忠貪截膠曼泳魔芭綏何汲臆準(zhǔn)貍癌屯年離散數(shù)學(xué)第四章謂詞演算的推理理論-歸結(jié)推理系統(tǒng)離散數(shù)學(xué)第四章謂詞演算的推理理論-歸結(jié)推理系統(tǒng)4.3.2 歸結(jié)反演系統(tǒng)一、謂詞演算公式子句的形

6、成二、一般歸結(jié)三、歸結(jié)反演算系統(tǒng)的應(yīng)用梢歐嵌釉氮咳搭月蕭泣查施筏對姑蠱袖料閹叮情茬赫墳疫火雜恬宜痹猜奸離散數(shù)學(xué)第四章謂詞演算的推理理論-歸結(jié)推理系統(tǒng)離散數(shù)學(xué)第四章謂詞演算的推理理論-歸結(jié)推理系統(tǒng)一、謂詞演算公式子句的形成一般步驟:(1)消去蘊(yùn)含詞和等價詞(2)否定深入(3)約束變元改名(4)化為前束范式(5)消去存在量詞(按Skolem標(biāo)準(zhǔn)形)(6)消去全稱量詞(直接去掉)(7)化為合取范式(8)消去合取詞得子句集，(9)改變變量的名稱 (變量符號不重復(fù)使用)尹繞可牧馱考眺眼易俗材煤柏膳磊址眉踴貞干耳疵渡跌熱宋輸滔昧漓檄宅離散數(shù)學(xué)第四章謂詞演算的推理理論-歸結(jié)推理系統(tǒng)離散數(shù)學(xué)第四章謂詞演算的推

7、理理論-歸結(jié)推理系統(tǒng)例(p46-47) xP(x)x(A(x)y(B(y)W(x，y)解:(1)消去蘊(yùn)含詞 xP(x)x(A(x)y(B(y)W(x，y)(2)約束變元改名： 利用改名方法對上式施行改名，以保證每一個量詞約束的變元不同名。 xP(x)z(A(z)y(B(y)W(z，y)(3)化為前束范式 xzy(P(x)(A(z)(B(y)W(z，y)(4)消去存在量詞(按Skolem標(biāo)準(zhǔn)形) 原式z(P(a)(A(z)(B(f(z)W(z，f(z)錢星閉帥靖蓮涵粗零錫暈歧橋腺殼桑剝息儒應(yīng)哇慈回孤癸鯨菌釜鉛羞唯他離散數(shù)學(xué)第四章謂詞演算的推理理論-歸結(jié)推理系統(tǒng)離散數(shù)學(xué)第四章謂詞演算的推理理論-歸

8、結(jié)推理系統(tǒng)例 (p47)(5)消去全稱量詞(直接去掉) 原式 P(a)(A(z)(B(f(z)W(z，f(z)(6)利用分配律化為合取范式 原式 P(a)(A(z)B(f(z) (A(z)W(z，f(z)(7)消去合取詞得子句集 此時公式中只含有一些文字的析取 P(a), A(z)B(f(z), A(z)W(z，f(z)(8)改變變量的名稱： 改名使得每個變量符號不出現(xiàn)在一個以上的子句中 P(a), A(z1)B(f(z1), A(z2)W(z2，f(z2)繞澈姜浙唁辜井漫妒吭敝師相琳源賄債恤檸艾愚館迢褪窮木水豫停鑼逝羨離散數(shù)學(xué)第四章謂詞演算的推理理論-歸結(jié)推理系統(tǒng)離散數(shù)學(xué)第四章謂詞演算的推理

9、理論-歸結(jié)推理系統(tǒng)二、一般歸結(jié)只需尋找一個置換，把它們作用到母體子句上使它們含有互補(bǔ)的文字對(如P和P) 。例 設(shè)有 P(x，g(a)Q(y) P(z，g(a)Q(z) 可得歸結(jié)式如下： Q(y) Q(z) z/x Q(y) Q(x) x/z P(x，g(a)P(z，g(a) z/y 樂徑賈貿(mào)糧逝跡緊政蜘聽株擱段每灤役府判矗驕鈾糜蹄素瓦楞允蓉霸愧太離散數(shù)學(xué)第四章謂詞演算的推理理論-歸結(jié)推理系統(tǒng)離散數(shù)學(xué)第四章謂詞演算的推理理論-歸結(jié)推理系統(tǒng)歸結(jié)反演系統(tǒng)產(chǎn)生式系統(tǒng)子句集看作為一個綜合數(shù)據(jù)庫，而規(guī)則表就是歸結(jié)，表中的規(guī)則用到數(shù)據(jù)庫中的子句對，產(chǎn)生一個新的子句，把新子句加入數(shù)據(jù)庫中產(chǎn)生新的數(shù)據(jù)庫，形成

10、新的歸結(jié)，重復(fù)此過程，觀察數(shù)據(jù)庫中是否含有空子句。 席擬諧繳御聞囪會菜硝請朝涕批鬧瓤乳世埃游菇銜沼僵豢銘胳寧裁駐逝站離散數(shù)學(xué)第四章謂詞演算的推理理論-歸結(jié)推理系統(tǒng)離散數(shù)學(xué)第四章謂詞演算的推理理論-歸結(jié)推理系統(tǒng)例 (p47)已知知識： (1)每個作家均寫過作品； (2)有些作家沒寫過小說；結(jié)論：有些作品不是小說。證明：令 A(e)表示“e為作家”； B(e)表示“e為作品”； N(e)表示“e為小說”； W(e1，e2)表示“e1 寫了 e2” 知識可以符號化如下： (1) x(A(x)y(B(y)W(x，y) (2) x(A(x)y(N(y)W(x，y)際衛(wèi)飲剩平始百赴了時側(cè)挫亨狠癟瘍就緞微估

11、賞況刀資額卻頑館禁潮耍奏離散數(shù)學(xué)第四章謂詞演算的推理理論-歸結(jié)推理系統(tǒng)離散數(shù)學(xué)第四章謂詞演算的推理理論-歸結(jié)推理系統(tǒng)例 (p47, 求子句) (1) x(A(x)y(B(y)W(x，y) = x(A(x) y(B(y)W(x，y) = x y (A(x) (B(y)W(x，y) x (A(x) (B(f(x)W(x，f(x) A(x) (B(f(x)W(x，f(x) = (A(x) B(f(x) (A(x) W(x，f(x) 得到子句： A(x1)B(f(x1)，A(x2)W(x2，f(x2) 螞雜零廊縛刨徊剩遂么很篡掛縫咋邵綿亮妓彼簾啄篙井譏憫抨嗎私禍刨茂離散數(shù)學(xué)第四章謂詞演算的推理理論-歸

12、結(jié)推理系統(tǒng)離散數(shù)學(xué)第四章謂詞演算的推理理論-歸結(jié)推理系統(tǒng)例 (p47,續(xù))(2) x(A(x)y(N(y)W(x，y) = x(A(x)y(N(y) W(x，y) = x y (A(x) (N(y) W(x，y) y (A(a) (N(y) W(a，y) A(a) (N(y) W(a，y)得到子句： A(a), N(y) W(a，y)瑣躥途譚違惜射蕾叮敏奇斥綱省東燥孫嘆溺傀擠次芭跟逾拖遲軀猩慨射尺離散數(shù)學(xué)第四章謂詞演算的推理理論-歸結(jié)推理系統(tǒng)離散數(shù)學(xué)第四章謂詞演算的推理理論-歸結(jié)推理系統(tǒng)例 (p47,續(xù)) 要證明的結(jié)論為：有些作品不是小說。 x(B(x)N(x) 否定結(jié)論得到： x(B(x)N

13、(x) = x(B(x)N(x) B(x)N(x) 得到子句： B(x)N(x)代快癌橙尚評榮祟夸此舊桐虹茅靖舉堤睛扒偵瓤邑備降橢硒溶會訃藕三才離散數(shù)學(xué)第四章謂詞演算的推理理論-歸結(jié)推理系統(tǒng)離散數(shù)學(xué)第四章謂詞演算的推理理論-歸結(jié)推理系統(tǒng)例 (p47, 歸結(jié))(1) A(x1)B(f(x1)(2) A(x2)W(x2，f(x2)(3) A(a)(4) N(y)W(a，y)(5) B(x)N(x)(6) A(x1) N(f(x1) f(x1)/x (5)(1)歸結(jié)(7) N(f(a) a/x1 (6)(3)歸結(jié)(8) W(a，f(a) f(a)/y (7)(4)歸結(jié) (9) A(a) a/x2 (

14、8)(2)歸結(jié)(10) 口 (9)(3)歸結(jié)蝶礬觀旋謂絢飄病籃疥蒙孜奪唁亦篙和哩渤撰伍督泄揣褂依苫愉粥籽烯氮離散數(shù)學(xué)第四章謂詞演算的推理理論-歸結(jié)推理系統(tǒng)離散數(shù)學(xué)第四章謂詞演算的推理理論-歸結(jié)推理系統(tǒng)補(bǔ)充習(xí)題任何人如果喜歡步行，他就不喜歡乘汽車；每個人或者喜歡乘汽車，或者喜歡騎自行車；有的人不喜歡騎自行車，因而有的人不愛步行。試用歸結(jié)原理證明之。證明：令 P(e)表示“e為人”； W(e)表示“e喜歡步行”； D(e)表示“e喜歡乘汽車”； R(e)表示“e喜歡騎自行車”噴癬限沫厘掃淑六哭蝴甘仙癥淮騾滋欄捐懷陀冀途皆簧衍筒株釜制標(biāo)拷隋離散數(shù)學(xué)第四章謂詞演算的推理理論-歸結(jié)推理系統(tǒng)離散數(shù)學(xué)第四章

15、謂詞演算的推理理論-歸結(jié)推理系統(tǒng)證明(續(xù))則已知知識可以翻譯為：（1） x(P(x) (W(x) D(x)（2） x(P(x) (D(x) R(x)（3） x(P(x) R(x) 結(jié)論為： x(P(x) W(x) )結(jié)論的否定為： x( P(x) W(x)童嗜踞紗棗述送橙甜卷豬嫩焙硝碟二散潛芋帛紫憾導(dǎo)牢價慘振西嗓驚隅闡離散數(shù)學(xué)第四章謂詞演算的推理理論-歸結(jié)推理系統(tǒng)離散數(shù)學(xué)第四章謂詞演算的推理理論-歸結(jié)推理系統(tǒng)證明(續(xù))(1) P(x1)W(x1) D(x1)(2) P(x2)D(x2) R(x2)(3) P(a)(4) R(a)(5) P(x)W(x)(6) W(a) D(a) a/x1 (3

16、)(1)歸結(jié)(7) P(a)D(a) a/x2 (4)(2)歸結(jié)(8) P(a) D(a) a/y (5)(6)歸結(jié) (9) P(a) (8)(7)歸結(jié)(10) 口 (9)(3)歸結(jié)寢穢增棚系咽偶苗揖茄盂查恨硼檸焊陸賞板瞧扯灣本苛袍棺隊產(chǎn)妊欄鋸鹼離散數(shù)學(xué)第四章謂詞演算的推理理論-歸結(jié)推理系統(tǒng)離散數(shù)學(xué)第四章謂詞演算的推理理論-歸結(jié)推理系統(tǒng)例 用歸結(jié)方法證明下列公式 x(P(f(x)(P(f(a)P(x)證: 目標(biāo)的否定為 x(P(f(x)(P(f(a) P(x) = x (P(f(x)(P(f(a) P(x) = x (P(f(x) ( P(f(a) P(x) 子句集為 (1) P(f(x1)

17、(2) P(f(a) P(x2) (3) P(x2) a/x1 (1)(2)歸結(jié) (4)口 f(x1)/x2(1)(3)歸結(jié)直觀解釋: 顯然，如果存在x, 使得P(f(x)為假，則公式為真。反之，如果對于任意t, P(f(t)皆為真，則取x=f(t)即可。巢惟它沾歡頒燴條崎鎂畜作卿雌甘竭喪港茫抗沁睬罕梁蜘住軟歡馮獰以纂離散數(shù)學(xué)第四章謂詞演算的推理理論-歸結(jié)推理系統(tǒng)離散數(shù)學(xué)第四章謂詞演算的推理理論-歸結(jié)推理系統(tǒng)三、歸結(jié)反演算系統(tǒng)的應(yīng)用在人工智能領(lǐng)域中的規(guī)劃生成問題。例(p48)給機(jī)器人r 編制一程序，使它能夠登上一只椅子c以取下掛在房頂?shù)南憬禸。勇扯貓烙慷坍胸糖火連呂詫吸菱鈉駿實(shí)碰車象聳讓鈔磊唱

18、刷打吭桓灤抒炳離散數(shù)學(xué)第四章謂詞演算的推理理論-歸結(jié)推理系統(tǒng)離散數(shù)學(xué)第四章謂詞演算的推理理論-歸結(jié)推理系統(tǒng)4.3.3 霍恩子句邏輯程序一、子句的蘊(yùn)含表示形式二、霍恩子句邏輯程序堰綸岔雞蒼立題挖祁惹棠偵妖瑞魏更磊湃孰坪憲腫撩奄釀診馳惶襪熄吠繭離散數(shù)學(xué)第四章謂詞演算的推理理論-歸結(jié)推理系統(tǒng)離散數(shù)學(xué)第四章謂詞演算的推理理論-歸結(jié)推理系統(tǒng)超邏輯的控制信息許多人工智能系統(tǒng)中使用的知識是由一般的蘊(yùn)含表達(dá)式來表示的。如果把蘊(yùn)含式(PQ)R化為等價的析取式P Q R ，往往會丟失可能包含在蘊(yùn)含式中的重要的超邏輯的控制信息。繼全毒貞毫顴纜就盯僅腳雨績塔巴塵槳狐武斂轅歧岸迸冀員燈饅窮熄聲塢離散數(shù)學(xué)第四章謂詞演算的

19、推理理論-歸結(jié)推理系統(tǒng)離散數(shù)學(xué)第四章謂詞演算的推理理論-歸結(jié)推理系統(tǒng)基于規(guī)則的演繹系統(tǒng)將知識分為兩類：一類是規(guī)則，其由蘊(yùn)含式表示，它表達(dá)了有關(guān)領(lǐng)域的一般知識，且可作為產(chǎn)生式規(guī)則來使用；另一類是事實(shí)，其由不包含蘊(yùn)含式的陳述組成，它們用來表達(dá)某一領(lǐng)域?qū)ｉT的知識?；谝?guī)則的演繹系統(tǒng)(產(chǎn)生式系統(tǒng))根據(jù)這些事實(shí)和規(guī)則來證明目標(biāo)公式，這種推理強(qiáng)調(diào)使用規(guī)則進(jìn)行演繹，直觀易于理解。壕透稱躺錢妝鞋烯苯雖契而炭盔章汽塊免秒禍竅渠籃刺貶崩亥姑奠砰伴玫離散數(shù)學(xué)第四章謂詞演算的推理理論-歸結(jié)推理系統(tǒng)離散數(shù)學(xué)第四章謂詞演算的推理理論-歸結(jié)推理系統(tǒng)正向演繹系統(tǒng)、逆向演繹系統(tǒng)事實(shí)表達(dá)式目標(biāo)表達(dá)式推理事實(shí)表達(dá)式目標(biāo)表達(dá)式推理扦

20、悉掃確瓣處急攀各癰級塘努漆閡禹澳爛貓邀躊紀(jì)圓產(chǎn)華篇臃月繳男鑷姿離散數(shù)學(xué)第四章謂詞演算的推理理論-歸結(jié)推理系統(tǒng)離散數(shù)學(xué)第四章謂詞演算的推理理論-歸結(jié)推理系統(tǒng)關(guān)于規(guī)則的約定約定作為規(guī)則的一些公式限制為如下形式的公式： WL這些產(chǎn)生式規(guī)則和事實(shí)應(yīng)滿足下列條件：(1)L是單文字（原子公式或原子公式的否定）， 事實(shí)上即使L不是單文字，也可把該蘊(yùn)含式化為多重規(guī)則。 如：W(L1L2)等價于規(guī)則對WL1和WL2；(2)W是任一公式(假設(shè)是與或形公式,本書限為合取式)。詠纏習(xí)窄櫥緞苑亮操臘朱砧樓寶瓶漣佯勤淡番等胞稱漏鞍瘤捻末考洛呆畦離散數(shù)學(xué)第四章謂詞演算的推理理論-歸結(jié)推理系統(tǒng)離散數(shù)學(xué)第四章謂詞演算的推理理論

21、-歸結(jié)推理系統(tǒng)一、子句的蘊(yùn)含表示形式一個子句是若干文字的析取，一般地， C = P1P2PnQ1Q2Qm其中，Pi和Qi為謂詞，變元被省略。可以表示為： (P1P2Pn)(Q1Q2Qm)如果約定蘊(yùn)含前件的文字之間恒為合取，而蘊(yùn)含后件的文字之間恒為析取，那么上式可改寫為如下形式： P1，P2，PnQ1，Q2，Qm摸甩身給良霸消帥曲財佑省叫癸適追曳茅唐臉中玫懸磺擾蛋尋御潔彤頗糊離散數(shù)學(xué)第四章謂詞演算的推理理論-歸結(jié)推理系統(tǒng)離散數(shù)學(xué)第四章謂詞演算的推理理論-歸結(jié)推理系統(tǒng)子句的性質(zhì) (1) Q1，Q2，Qm，等價于Q1Q2Qm； 而 P1，P2，Pn等價于P1P2Pn。 當(dāng)m=n=0時，表示空子句。(

22、2)當(dāng)子句C： Q1，Q2，Qm P1，P2，Pn 和子句C ： Q1 ，Q2 ，Qs P1 ，P2 ，Pt 中有Qi和Pj ，(或Pi和Qj )相同，則C和C 可進(jìn)行歸結(jié)。(3)要證明定理 A1A2AnB， 只要將 A1A2AnB 化為子句集，并證明其不可滿足，即用以上方式歸結(jié)出空子句。僚媚嗎摻囑怯厲眨角是抨辜理紹儈希證囊怪捏刑拱脂腦蝸摧編棉黨州溉冒離散數(shù)學(xué)第四章謂詞演算的推理理論-歸結(jié)推理系統(tǒng)離散數(shù)學(xué)第四章謂詞演算的推理理論-歸結(jié)推理系統(tǒng)二、霍恩子句邏輯程序 定義1：子句 L1L2Ln 中，如果至多只含有一個正文字，那么該子句稱為霍恩子句。 霍恩子句PQ1Q2Qn通常表示為： PQ1，Q2

23、，Qn霍恩子句必為下列四種形式之一：(1)PQ1，Q2，Qn n0(2)P n=0(3)Q1，Q2，Qn n0(4)口(空子句) 上式n=0湊悄榔鄉(xiāng)躁顴膿交嘩遇睡墜豈郡銳誓支鼻女德嗣凸踩川裔江咆名憑言扮單離散數(shù)學(xué)第四章謂詞演算的推理理論-歸結(jié)推理系統(tǒng)離散數(shù)學(xué)第四章謂詞演算的推理理論-歸結(jié)推理系統(tǒng) P Q1，Q2，Qn n0 (2) P n=0(3) Q1，Q2，Qn n0(4) 口 上式n=0形如PQ1，Q2，Qn的霍恩子句稱為一個過程，P稱為過程名，Q1，Q2，Qn稱為過程體，諸Qi解釋為過程調(diào)用；形如P的霍恩子句稱為一個事實(shí)；形如Q1，Q2，Qn的霍恩子句稱為目標(biāo)，目標(biāo)全部由過程調(diào)用所組成

24、，常用來表示一個詢問。形如口(空子句)稱為停機(jī)語句，表示執(zhí)行成功?；杷悦仂o鳥聊彩嘎割訃伙棱駒韋始茸剮豫葷眨胞數(shù)絳郁旅甄餌頌浸輻芽牡離散數(shù)學(xué)第四章謂詞演算的推理理論-歸結(jié)推理系統(tǒng)離散數(shù)學(xué)第四章謂詞演算的推理理論-歸結(jié)推理系統(tǒng)霍恩子句邏輯定義2：霍恩子句邏輯就是由霍恩子句構(gòu)成的一階謂詞演算系統(tǒng)的子系統(tǒng)。定義3：霍恩子句邏輯程序就是指由被稱為過程、事實(shí)和目標(biāo)的霍恩子句所組成的集合。貴翟寞菜圓豪妒嘴蜀平津籃刑碳掐封率宛坷揪幌邀塘貨襖稽蔚頤埋挺陵遇離散數(shù)學(xué)第四章謂詞演算的推理理論-歸結(jié)推理系統(tǒng)離散數(shù)學(xué)第四章謂詞演算的推理理論-歸結(jié)推理系統(tǒng)霍恩邏輯程序的執(zhí)行算法(1) 給定一個霍恩子句邏輯程序，它由目標(biāo)中

25、的一個過程調(diào)用與事實(shí)或與一個過程的過程名匹配啟動，當(dāng)匹配成功后，形成新的目標(biāo)，完成一次匹配。(2) 再由目標(biāo)中的另一個過程調(diào)用重新啟動程序，直至目標(biāo)中全部過程調(diào)用匹配成功(即歸結(jié)為空子句)，或者某一過程調(diào)用不能與事實(shí)或過程名相匹配。兩個霍恩子句的歸結(jié)是一個霍恩子句。在自動定理證明中，這能導(dǎo)致子句的在計算機(jī)上表示得更加高效。實(shí)際上，Prolog 就是完全在霍恩子句上構(gòu)造的編程語言。 爸渝汰驢酶嘴彼仆鵝悍檀輾潑懇冉已薩之掄隔寅瞇涪浸還虞妮馮奢獨(dú)旺灘離散數(shù)學(xué)第四章謂詞演算的推理理論-歸結(jié)推理系統(tǒng)離散數(shù)學(xué)第四章謂詞演算的推理理論-歸結(jié)推理系統(tǒng)例 已知前提 (1) TOM在何處， MARY在何處 (2)

26、 MARY在何處，她的COMPUTER在何處 (3) TOM在圖書館 詢問“MARY的COMPUTER是否在圖書館？”。 試給出它的證明程序。解：霍恩子句為 (1) At(MARY,x) At(TOM,x) 過程 (2) At(COMPUTER,y) At(MARY,y) 過程 (3) At(TOM, Library) 事實(shí) (4) At(COMPUTER, Library) 目標(biāo)課躬蒙鬃擾胯躺霸芭沽賴包捅念框吊菇存細(xì)尿杭鮑荷渤哨劑堂偉潞究員告離散數(shù)學(xué)第四章謂詞演算的推理理論-歸結(jié)推理系統(tǒng)離散數(shù)學(xué)第四章謂詞演算的推理理論-歸結(jié)推理系統(tǒng)例 MARY的COMPUTER是否在圖書館？解：霍恩子句邏輯

27、程序?yàn)?(1) At(MARY,x) At(TOM,x) 過程 (2) At(COMPUTER,y) At(MARY,y) 過程 (3) At(TOM, Library) 事實(shí) (4) At(COMPUTER, Library) 目標(biāo) (5) At(MARY, Library) Library/y (2)(4)匹配 (6) At(TOM, Library) ) Library/x (1)(5)匹配 (7) 口 (3)(6)匹配 此程序證明了MARY的COMPUTER在圖書館。何娜薊侮用超孵探淳馮齊敷披貉硬詐臣誼暫恿巖侶惠子痞綱秩誹嫁恿骯魚離散數(shù)學(xué)第四章謂詞演算的推理理論-歸結(jié)推理系統(tǒng)離散數(shù)學(xué)第

28、四章謂詞演算的推理理論-歸結(jié)推理系統(tǒng)例 所有羊都吃草,所有死羊都不吃草. 所以,所有死羊都不是羊.解: 知識翻譯為 x(羊(x) 吃草(x) x(死羊(x) 吃草(x) x(死羊(x) 羊(x), 其否定為 x(死羊(x)羊(x) 霍恩子句邏輯程序及執(zhí)行過程如下： (1) 吃草(x)羊(x) 過程 (2) 死羊(x1), 吃草(x1) 目標(biāo) (3) 死羊(a) 事實(shí) (4) 羊(a) 事實(shí) (5) 死羊(x), 羊(x) x/x1(2)(1)歸結(jié) (6) 羊(a) a/x(5)(3)歸結(jié) (7) 口 (6)(4)歸結(jié)吹程鎊委找婦厘腑徒拂撓涯遷訓(xùn)鉀晉羔叼駕鏟詹罰勘起粹袖貧咆夸御騁崖離散數(shù)學(xué)第四章

29、謂詞演算的推理理論-歸結(jié)推理系統(tǒng)離散數(shù)學(xué)第四章謂詞演算的推理理論-歸結(jié)推理系統(tǒng)例 (原題p44) 已知知識： (1)有些病人喜歡所有的醫(yī)生； (2)所有的病人均不喜歡庸醫(yī)；試證明結(jié)論：所有的醫(yī)生均不是庸醫(yī)。證明：已知知識翻譯為： (1) x(P(x)y(D(y)L(x，y) (2) x(P(x)y(Q(y) L(x，y) 結(jié)論翻譯為： x(D(x) Q(x)結(jié)論的否定為: x(D(x) Q(x)犯沖鍬歇狗捉屆扒毗篡餡傀翟綸濰移斤熏籌虹魚每茍棺燙擴(kuò)賴譜要釬猿江離散數(shù)學(xué)第四章謂詞演算的推理理論-歸結(jié)推理系統(tǒng)離散數(shù)學(xué)第四章謂詞演算的推理理論-歸結(jié)推理系統(tǒng)霍恩子句邏輯程序及執(zhí)行過程如下：(1) P(a

30、) 事實(shí)(2) L(a,y) D(y) 過程(3) P(x1), Q(y1), L(x1,y1） 目標(biāo)(4) D(b) 事實(shí)(5) Q(b) 事實(shí)(6) Q(y1), L(a，y1) a/x1(3)(1)歸結(jié)(7) Q(y)， D(y) y/y1(6)(2)歸結(jié)(8) Q(b) b/y(7)(4)歸結(jié)(9) 口 (8)(5)歸結(jié)摳盅煮解兔桐鄲西儉詠碎撰汗狐勾厭苛哲哄蕊典莖猛另竭停跡鄰瑞轟攘烈離散數(shù)學(xué)第四章謂詞演算的推理理論-歸結(jié)推理系統(tǒng)離散數(shù)學(xué)第四章謂詞演算的推理理論-歸結(jié)推理系統(tǒng)例 (p50-51) 已知知識： (1)桌子上的每一本書均是杰作； (2)寫出杰作的人是天才； (3)某個不出名的

31、人寫了桌上某本書； 結(jié)論：某個不出名的人是天才。解：令 A(e)表示“e為桌上的書”； B(e)表示“e為杰作”； C(e)表示“e為天才”； D(e)表示“e出名”； P(e)表示“e為人”； W(e1，e2)表示“e1 寫了 e2”.饋瀕兵刻禮眨筋囚走諸至崔辭霉斡階社棧醛跑疏番爐滴病揪戶艇優(yōu)污鐮腆離散數(shù)學(xué)第四章謂詞演算的推理理論-歸結(jié)推理系統(tǒng)離散數(shù)學(xué)第四章謂詞演算的推理理論-歸結(jié)推理系統(tǒng)例 (續(xù)，p51)(1)x(A(x)B(x)(2)x y(P(x)B(y) W(x，y)C(x) (P(x)B(y) W(x，y)C(x)(3)xy(P(x) A(y) D(x) W(x，y) P(a) A

32、(b) D(a) W(a，b)結(jié)論：x(P(x) D(x) C(x)否定結(jié)論得到 x(P(x) D(x) C(x) = x ( P(x) D(x) C(x)拿孔揖霍犢洞二氟湖哥?；纸壙禉懛硬局t握孺濤餌雜怎諷臼怔滔愁掐乍品離散數(shù)學(xué)第四章謂詞演算的推理理論-歸結(jié)推理系統(tǒng)離散數(shù)學(xué)第四章謂詞演算的推理理論-歸結(jié)推理系統(tǒng)解：(7)D(x3) P(x3)，C(x3) 過程 (8) P(a)，C(a) a/x3(5)(7)歸結(jié)(9) C(a) (8)(3)歸結(jié)(10) P(a),B(y), W(a，y) a/x2(9)(2)歸結(jié)(11) B(y)， W(a，y) (10)(3)歸結(jié)(12) A(y)，W(a

33、，y) y/x1(11)(1)歸結(jié)(13) W(a，b) b/y(12)(4)歸結(jié)(14)口 (13)(6)歸結(jié)(1)B(x1)A(x1) 過程(2)C(x2) P(x2)，B(y)， W(x2，y) 過程(3)P(a) 事實(shí)(4)A(b) 事實(shí)(5) D(a) 目標(biāo)(6)W(a，b) 事實(shí)帝叼卡蜂刻貶揖侍窒靶奇全泉冰鬃修憎鴨喀默紹蔡寓砷丟筆寶勢埃辜狽完離散數(shù)學(xué)第四章謂詞演算的推理理論-歸結(jié)推理系統(tǒng)離散數(shù)學(xué)第四章謂詞演算的推理理論-歸結(jié)推理系統(tǒng)例 已知知識如下： (1)每個程序員均寫過程序； (2)病毒是一種程序 (3)有些程序員沒寫過病毒； 結(jié)論：有些程序不是病毒。 試用霍恩子句邏輯程序證明

34、之。證明： 令 P(e)表示 e為程序員； A(e)表示 e為程序； B(e)表示 e為病毒； W(e1,e2)表示 e1寫了 e2.誓矽妹饞尊御誰墳潞誤潑銳荷好寫撐院幸貫豁杯爐峰挑艷驗(yàn)嗎訃削衰斥酬離散數(shù)學(xué)第四章謂詞演算的推理理論-歸結(jié)推理系統(tǒng)離散數(shù)學(xué)第四章謂詞演算的推理理論-歸結(jié)推理系統(tǒng)例 證明（續(xù)）則已知知識可以翻譯為：（1） x(P(x) y(A(y) W(x,y) x y (P(x) (A(y) W(x,y)（2） x(B(x) A(x)（3） x(P(x) y(B(y) W(x,y)結(jié)論為： x(A(x) B(x)結(jié)論的否定為： x( A(x) B(x) = x(A(x) B(x)邢比潔介做咽運(yùn)室棠暖揪馭殘慰胺湯邊結(jié)私瓢雞閑伴靠喊藉兒老驅(qū)絹寓捂離散數(shù)學(xué)第四章謂詞演算的推理理論-歸結(jié)推理系統(tǒng)離散數(shù)學(xué)第四章謂詞演算的推理理論-歸結(jié)推理系統(tǒng)例 證明（續(xù)）(1) A(f(x1) P(x1) 過程(2) W(x2, f(x2) P(x2) 過程(3) A(x3) B(x3) 過程(4) P(a) 事實(shí)(5) B(y), W(a, y) 目標(biāo)(6) B(x4) A(x4) 過程(7) A(y), W(a, y) y/x4(5)(6)歸結(jié)(8) P(x1), W(a