計(jì)算引論6 推理與計(jì)算

1、第四章 推理與計(jì)算1主要內(nèi)容邏輯與推理Horn邏輯程序命題Horn邏輯中的自動(dòng)推理謂詞Horn邏輯中的自動(dòng)推理 Prolog邏輯 程序設(shè)計(jì)24.1 邏輯基礎(chǔ)知識(shí) 符號(hào)表示：常量：小寫字母 a, b, c,.。 函數(shù)：小寫字母 f, g, h,. 。 變量：小寫字母 x, y, z,.。 邏輯算子(或連結(jié)詞)：, , , , 。 量詞： , . 謂詞：大寫字母 P, Q, R,. 。34.1 邏輯基礎(chǔ)知識(shí) 命題：在一階邏輯中，命題陳述某個(gè)對(duì)象的性質(zhì)，或是某些對(duì)象的關(guān)系，是能夠分辨真假的語(yǔ)句。原子命題：一個(gè)語(yǔ)句如果不能再進(jìn)一步分解成更簡(jiǎn)單的語(yǔ)句，并且又是一個(gè)命題，則稱此命題為原子命題4命題公式：原

2、子命題是命題公式。若A是命題公式，則 A也是命題公式。若A和B都是命題公式，則AB、AB、 A B、AB是命題公式。 5命題公式的缺點(diǎn)： 無(wú)法把所描述的客觀事物的結(jié)構(gòu)和邏輯特征反映出來(lái)不能把不同事物的共同特征反映出來(lái)例如： 命題P:“張三是李四的老師”6謂詞邏輯： 在謂詞邏輯中，將原子命題分解為謂詞與個(gè)體兩部分。個(gè)體是指可以獨(dú)立存在的物體，可以是抽象的或具體的。謂詞則是用于刻畫個(gè)體的性質(zhì)、狀態(tài)或個(gè)體間的關(guān)系的。 7 謂詞的一般形式：P(x1,x2,xn ) 其中P是謂詞，x1,x2,xn是個(gè)體。例：“鳥會(huì)飛”可表示為canfly(bird).其中canfly是謂詞，bird是個(gè)體。 8謂詞分類

3、：一元謂詞：刻畫個(gè)體的性質(zhì)多元謂詞：刻畫個(gè)體之間的關(guān)系一階謂詞：個(gè)體是常量、變?cè)唠A謂詞：個(gè)體是謂詞9項(xiàng)定義如下：?jiǎn)蝹€(gè)的常量和變量都是項(xiàng)。如果f是函數(shù)符, t1, tn是項(xiàng)，那么 f(t1, tn)也是項(xiàng)。 例如，gcd是表示最大公約數(shù)的函數(shù)符，a+b，cd-2是兩個(gè)項(xiàng)，則gcd(a+b,cd-2)也是項(xiàng)。10原子： 若P是一個(gè)n元謂詞符號(hào)，t1, tn是項(xiàng),那么P(t1, tn)是原子 。例如，father是表示父子關(guān)系的二元謂詞，則father(John, Peter)是原子，表示John是Peter的父親。這里 father(John, Peter)做為基本二元關(guān)系。11謂詞公式： 原子

4、是公式 若P,Q是公式，則 PQ, PQ, PQ, PQ, P 是公式。 若P是公式，x是P中的變量，則 (x)P，(x)P 是公式。 12文字： 若P是原子，則P, P稱為文字。P稱為正文字，P稱為負(fù)文字。子句： 公式P稱為子句，若P為L(zhǎng)1Ln，其中L1,Ln是文字。基項(xiàng)、基原子、基子句： 沒有變量符號(hào)出現(xiàn)的項(xiàng)、原子、子句， 分別稱為基項(xiàng)、基原子、基子句。13例: gcd(45, b)是基項(xiàng) father(John, Peter)是基原子 father(John, Peter) uncle(John, Peter) 是基子句14謂詞公式的解釋 設(shè)D為謂詞公式P的個(gè)體域，若對(duì)P中的個(gè)體常量、函

5、數(shù)和謂詞按照如下規(guī)定賦值：（1）為每個(gè)個(gè)體常量指派D中的一個(gè)元素；（2）為每個(gè)n元函數(shù)指派一個(gè)從Dn到D的映射，其中 Dn=(x1,x2,xn)|x1,x2,xn D（3）為每個(gè)n元謂詞指派一個(gè)從Dn到F,T的映射；則稱這些指派為公式P在D上的一個(gè)解釋。15永真：如果謂詞公式P，對(duì)個(gè)體域D上的任何一個(gè)解釋都取得真值T，則稱P在D上是永真的。如果P在每個(gè)非空個(gè)體域上均永真，則稱P永真。16永假（不可滿足性）如果謂詞公式P對(duì)于個(gè)體域D上的所有解釋都取得假值F，則稱P在D上是永假的；如果P在每個(gè)非空個(gè)體域上均永假，則稱P永假。17可滿足的：對(duì)于謂詞公式P，如果至少存在一個(gè)解釋使得公式P在此解釋下的真

6、值為T，則稱公式P是可滿足的。不可滿足的：對(duì)謂詞公式P，如果不存在任何解釋，使得P的取值為T，則稱公式P是不可滿足的。184.2 推理相關(guān)知識(shí)推理： 指從已知事實(shí)出發(fā)，運(yùn)用已掌握的知識(shí)，推導(dǎo)出其中蘊(yùn)含的事實(shí)性結(jié)論或歸納出某些新的結(jié)論的過(guò)程。推理分類：自然演繹：已知事實(shí) 推理規(guī)則 結(jié)論歸結(jié)：否定結(jié)論 前提條件 矛盾19Skolem化： 公式形式是很多樣的。這就會(huì)給機(jī)器的形式化處理帶來(lái)很大的麻煩。為了便于機(jī)器處理，把公式化成統(tǒng)一的標(biāo)準(zhǔn)形式，即SKOLEM標(biāo)準(zhǔn)型。20Skolem標(biāo)準(zhǔn)型： 設(shè)P是公式，P等價(jià)于x1xnG(x1. xn)，并且GG1Gm，其中G1,Gm都是子句，則稱G的子句集S = G

7、1,Gm 為公式P的Skolem標(biāo)準(zhǔn)型。21對(duì)公式P的SKOLEM化的步驟如下：（1）將P化為前束范式（Q1x1）（Qnxn）H(x1. xn) 其中 Q1Qn是存在量詞或者全稱量詞，H為合取范式的形式,不含, ； 22（2）用如下方法消去存在量詞： i) 若Qi是一個(gè)存在量詞，并且它的左邊沒有全稱量詞，則用一個(gè)H中沒有的常量符號(hào)代替H中所有的xi，之后消去（Qixi） 23ii) 若Qi是一個(gè)存在量詞，并且Qj1,Qjk是Qi左邊的全稱量詞，則取一個(gè)H中沒有的函數(shù)k元符號(hào)f, 用f(xj1,xjk)代替xi,之后消去（Qixi）。 24公式P經(jīng)過(guò)如上處理，可以化為x1xn(G1Gm) 的形式

8、，其中G1,Gm都是子句。省略全稱量詞，再用“，”取代合取符號(hào)，便得到公式P的Skolem標(biāo)準(zhǔn)型G1,Gm 。 25任意公式都有與之相對(duì)的子句集。一個(gè)公式與它的Skolem標(biāo)準(zhǔn)型未必等值，但在不可滿足的意義上是一致的。 26置換：是形如t1/x1, tn/xn的一個(gè)有限集合。其中xi（i=1,n） 是兩兩不同的變量符號(hào), ti是不同于xi的項(xiàng)。置換作用于表達(dá)式： 給定置換=t1/x1, tn/xn和表達(dá)式E，E表示將E中出現(xiàn)的每一個(gè)xi（i=1,n）都替換成ti得到的新表達(dá)式。27給定兩個(gè)置換 =t1/x1, tn/xn =u1/y1, um/ym 將集合 t1/x1, tn /xn ,u1/

9、y1, um/ym 刪去以下元素： ui/yi，當(dāng)yi x1, xn ti /xi，當(dāng)ti =xi 得到的新置換表示為 ，稱為 和 的復(fù)合 。 28 置換滿足結(jié)合律 ( ) = ( ) 置換不滿足交換律 = = 29合一置換： 給定表達(dá)式E1,Ek，若存在置換 ，使得E1=Ek ，則稱是E1,Ek的一個(gè)合一置換。 30 例1：設(shè)E1=g(x,y)，E2=g(a,f(z)。令 =a/x, f(h(u)/y, h(u)/z， 則E1=g(a, f(h(u), E2=g(a, f(h(u) 因?yàn)镋1=E2，所以是E1與E2的合一 置換。31例2，設(shè)E1與E2同上，=a/x, f(z)/y，則 E1=

10、g(a, f(z)=E2，所以也是E1與E2的合一置換。 顯然比 簡(jiǎn)單，易證= ，其中=h(u)/z32 最一般合一置換求法：設(shè)有公式：E1=P(x,y,z); E2= P(x,f(a),g(b)從左至右查找不同的項(xiàng)，構(gòu)成了不一致集： D1=y,f(a)繼續(xù)向右比較又得到一個(gè)不一致集： D2=z,g(b)置換為 = f(a)/y, g(b)/z33 求一般置換算法：令W= E1,E2 令 k=0,Wk=W,k=;是空置換, 表示不作置換。如果Wk只有一個(gè)表達(dá)式，則算法停止，k就是所要求的結(jié)果.找出Wk的不一致集Dk 。 若Dk中存在元素xk和tk ，其中xk是變?cè)?，tk是項(xiàng)，且xk不在tk中出

11、現(xiàn)，則： k+1=k tk/xk Wk+1=wktk/xk k=k+1 然后轉(zhuǎn)（2）。算法終止，W的一般合一置換不存在。34可以證明，如果E1和E2可合一，則算法必停止于第2步。354.2 Horn邏輯程序人工智能： 知識(shí)庫(kù)：用于推理的知識(shí) 數(shù)據(jù)庫(kù)：事實(shí)和論據(jù) 推理：對(duì)知識(shí)和數(shù)據(jù)的消解，獲得結(jié)論364.2 Horn邏輯程序已知的知識(shí)表示方法有產(chǎn)生式表示法語(yǔ)義網(wǎng)絡(luò)表示法邏輯表示法產(chǎn)生式表示法是一類很重要的方法，知識(shí)表示成IF THEN 的形式。采用產(chǎn)生式方法，可以將規(guī)則與事實(shí)以統(tǒng)一的格式表示，即Horn子句。374.2 Horn邏輯程序如果在一個(gè)子句中最多含有一個(gè)正文字，那么該子句稱為Horn子

12、句。若一個(gè)子句集內(nèi)的子句個(gè)數(shù)有限且都是Horn子句，那么該子句集稱為一個(gè)Horn邏輯程序。384.2 Horn邏輯程序Horn子句可以表示成如下形式：規(guī)則體規(guī)則頭 其中規(guī)則體一般是n個(gè)原子的合取， n=0,1,。規(guī)則頭可以是單個(gè)原子，也可以是空。394.2 Horn邏輯程序規(guī)則：規(guī)則體非空且規(guī)則頭非空的子句。例如， father(z, y), father(y, x)grandfather(z, x)事實(shí)：規(guī)則體空且規(guī)則頭非空的子句。例如，father(John, Peter)。目標(biāo)：無(wú)規(guī)則頭的子句，例如，grandfather(Smith, Peter)，即要查詢Smith是否是Peter的

13、祖父？404.2 Horn邏輯程序一個(gè)Horn邏輯程序是Horn子句的集合，也就是規(guī)則和事實(shí)的集合。因此，一個(gè)Horn邏輯程序相當(dāng)于一個(gè)知識(shí)庫(kù)。推理即是通過(guò)對(duì)一組子句按照一定的方式進(jìn)行消解最終得到新的公式。41自動(dòng)推理的過(guò)程即給定目標(biāo)子句，機(jī)器按照一定的順序?qū)壿嫵绦蛑械淖泳溥M(jìn)行消解，最后得到目標(biāo)子句，或者得出目標(biāo)不可滿足的結(jié)論。42命題Horn邏輯的自動(dòng)推理謂詞Horn邏輯的自動(dòng)推理434.3 命題Horn邏輯中的自動(dòng)推理 在命題Horn邏輯中，子句之間可以按照如下的方式消解。若有子句S1：A1,AnS2：B1,Bm Ai 則歸結(jié)后的子句為 S3：A1,Ai-1, B1,Bm, Ai+1,A

14、n 即利用規(guī)則S2將原目標(biāo)S1轉(zhuǎn)化為新目標(biāo)S3.444.3 命題Horn邏輯中的自動(dòng)推理基于上述消解方式，求證一個(gè)目標(biāo)S：A1,An 需要逐一以S的體中的每一個(gè)原子Ai作為新的目標(biāo)進(jìn)行求證。 A1,An 也稱為S的子目標(biāo)。在以一個(gè)原子Ai為目標(biāo)進(jìn)行求證時(shí)，考察子句集內(nèi)所有頭部是Ai的子句，以此子句的體作為新的目標(biāo)。 454.3 命題Horn邏輯中的自動(dòng)推理當(dāng)某個(gè)關(guān)于A的子句體部的所有原子得到滿足時(shí)，直接返回A是正確的，而不用再接著考察頭是A的其他子句。假如對(duì)于某個(gè)原子A，邏輯程序中所有頭部是A的子句都無(wú)法滿足，則得出A無(wú)法滿足的結(jié)論。 46原子A的推理算法TorF(A)如下：TorF(A) i

15、=0; while (in) /n是此Horn邏輯程序內(nèi)子句的個(gè)數(shù) if (第i條規(guī)則的頭部=A) /用第i條規(guī)則考察A if (第i條規(guī)則的體是空的) then return 1; / A是 事實(shí) else if ( TorF(A1)= = TorF(Am)=1) /A1 Am 是第i條規(guī)則體內(nèi)的所有原子 then return 1; /由i規(guī)則推出原子A的正確 i=i+1; /第i條規(guī)則體內(nèi)并非所有原子正確，從而需 要考察別的規(guī)則 return 0; /考察了所有的規(guī)則，都不能推出A 474.4 謂詞Horn邏輯中的自動(dòng)推理 謂詞Horn邏輯的消解要復(fù)雜一些。消解方式如下。若有子句S1：A

16、1,An S2：B1,BmB， 并且Ai, B具有合一置換，則歸結(jié)后的子句為S3：(A1,Ai-1,B1,Bm, Ai+1,An) 與命題Horn邏輯相比，需要考慮項(xiàng)的匹配，即合一問題。484.4 謂詞Horn邏輯中的自動(dòng)推理 基于以上消解方式，求證一個(gè)目標(biāo)S1：A1,An 時(shí)，要求得出的結(jié)果應(yīng)該是一個(gè)置換的集合。集合內(nèi)的每一個(gè)元素i應(yīng)該使A1i, , Ani 成立。494.4 謂詞Horn邏輯中的自動(dòng)推理在以一個(gè)原子Ai為目標(biāo)進(jìn)行考察時(shí)，考察每一個(gè)頭部是Ai的子句，以此子句的體作為新的目標(biāo)。返回的不是0（假）或者1（真），而應(yīng)是一個(gè)置換的集合。為此先要給出置換算法Substitution以及

17、求表達(dá)式合一算法Unify。 50 4.4 謂詞Horn邏輯中的自動(dòng)推理將置換作用于表達(dá)式e的算法如下Substitution(e, ) if (e是常量符號(hào)) then return e; if (e是變量符號(hào)x) then if (t/x) then return t else return e; if (e=f(t1,tn) then t1= Substitution(t1, ); tn= Substitution(tn, ) return f(t1,tn) 514.4 謂詞Horn邏輯中的自動(dòng)推理對(duì)兩個(gè)表達(dá)式e1，e2作合一的算法如下/算法返回一個(gè)合一置換或“無(wú)法合一”的信息Unify

18、(e1，e2) =空集； if e1是變量符號(hào)x then = e2/x; else if e2是變量符號(hào)x then = e1/x; else if(e1是常量而e2不是，或e2是常量而e1不是， 或 e1，e2是兩個(gè)不同的常量) then return “無(wú)法合一” else /此時(shí)e1，e2形如f(t1,tn)和 g(s1,sm)；f,g為函數(shù)符號(hào)。524.4 謂詞Horn邏輯中的自動(dòng)推理 if (fg) then return “無(wú)法合一”; else 1= Unify(t1，s1); = 1; 2= Unify(Substitution(t2, ), Substitution(s2,

19、 ); = 2; n= Unify(Substitution(tn, )，Substitution(sn, ); = n; return ; 534.4 謂詞Horn邏輯中的自動(dòng)推理例：Horn邏輯程序（知識(shí)庫(kù)）如下， father(z, y), father(y, x)grandfather(z, x)， father(John, Peter)， father(Smith, John)。 目標(biāo)為grandfather(Smith, Peter)，即查詢Smith是否是Peter的祖父？544.4 謂詞Horn邏輯中的自動(dòng)推理推理過(guò)程如下；1. 首先通過(guò)合一置換=Peter/x, Smith/

20、z，將目標(biāo)與知識(shí)庫(kù)中第一條規(guī)則的規(guī)則頭匹配，得到新目標(biāo) father(Smith, y), father(y, Peter) 2. 考察知識(shí)庫(kù)中第二條和第三條規(guī)則，通過(guò)合一置換=John/y與知識(shí)庫(kù)中的事實(shí)匹配 father(Smith, John), father(John, Peter) 因此查詢目標(biāo)成立，并且返回置換 =Peter/x, John/y, Smith/z 554.4 謂詞Horn邏輯中的自動(dòng)推理考察某個(gè)原子A的算法TorF(A)如下 TorF(A)輸入A(s1,sn), 返回置換數(shù)組, 其中數(shù)組元素i是一個(gè)置換。56 TorF(A) i=0； =空集； while(i0 /

21、 下面i1, i2,im初值均為1 while(TorF(A1)i1!=NULL) 1=TorF(A1)i1; i1=i11;57 while(TorF(A21)i2!=NULL) while(TorF(Am m-1)im!=NULL) m=TorF(A1)im; = 1 m; = ； im im +1; L1: i=i+1; /考察下一條規(guī)則 return ; 58PrologProlog(Programming in logic)語(yǔ)言是以Horn子句邏輯為基礎(chǔ)的高級(jí)程序設(shè)計(jì)語(yǔ)言。1972年，法國(guó)馬賽大學(xué)的Alain. Colmerauer提出了Prolog的雛型。1975年，Prolog被用于問題求解系統(tǒng)。59事實(shí)：關(guān)于對(duì)象性質(zhì)和關(guān)系的事實(shí)語(yǔ)句；student(john)，married(tom,mary)規(guī)則：關(guān)于對(duì)象性質(zhì)和關(guān)系的定義規(guī)則語(yǔ)句；B: A“如果A則B”bird