計算引論 推理與計算

計算引論推理與計算第一頁，共六十四頁，2022年，8月28日主要內容邏輯與推理Horn邏輯程序命題Horn邏輯中的自動推理謂詞Horn邏輯中的自動推理

Prolog邏輯

程序設計第二頁，共六十四頁，2022年，8月28日4.1邏輯基礎知識符號表示：常量：小寫字母a,b,c,...。函數：小寫字母f,g,h,...。變量：小寫字母x,y,z,...。邏輯算子(或連結詞)：,,,→,?。量詞：,.謂詞：大寫字母P,Q,R,...。第三頁，共六十四頁，2022年，8月28日4.1邏輯基礎知識命題：在一階邏輯中，命題陳述某個對象的性質，或是某些對象的關系，是能夠分辨真假的語句。原子命題：一個語句如果不能再進一步分解成更簡單的語句，并且又是一個命題，則稱此命題為原子命題第四頁，共六十四頁，2022年，8月28日命題公式：原子命題是命題公式。若A是命題公式，則A也是命題公式。若A和B都是命題公式，則A∧B、A∨B、

A→B、A?B是命題公式。

第五頁，共六十四頁，2022年，8月28日命題公式的缺點：無法把所描述的客觀事物的結構和邏輯特征反映出來不能把不同事物的共同特征反映出來例如：命題P:“張三是李四的老師”第六頁，共六十四頁，2022年，8月28日謂詞邏輯：在謂詞邏輯中，將原子命題分解為謂詞與個體兩部分。個體是指可以獨立存在的物體，可以是抽象的或具體的。謂詞則是用于刻畫個體的性質、狀態(tài)或個體間的關系的。第七頁，共六十四頁，2022年，8月28日

謂詞的一般形式：P(x1,x2,…,xn)其中P是謂詞，x1,x2,…,xn是個體。例：“鳥會飛”可表示為canfly(bird).其中canfly是謂詞，bird是個體。

第八頁，共六十四頁，2022年，8月28日謂詞分類：一元謂詞：刻畫個體的性質多元謂詞：刻畫個體之間的關系一階謂詞：個體是常量、變元高階謂詞：個體是謂詞第九頁，共六十四頁，2022年，8月28日項定義如下：單個的常量和變量都是項。如果f是函數符,t1,…,tn是項，那么f(t1,…,tn)也是項。

例如，gcd是表示最大公約數的函數符，a+b，c×d-2是兩個項，則gcd(a+b,cd-2)也是項。第十頁，共六十四頁，2022年，8月28日原子：

若P是一個n元謂詞符號，t1,…,tn是項,那么P(t1,…,tn)是原子。例如，father是表示父子關系的二元謂詞，則father(John,Peter)是原子，表示John是Peter的父親。這里father(John,Peter)做為基本二元關系。第十一頁，共六十四頁，2022年，8月28日謂詞公式：

原子是公式

若P,Q是公式，則P→Q,P?Q,P∧Q,P∨Q,P是公式。

若P是公式，x是P中的變量，則(x)P，(x)P是公式。第十二頁，共六十四頁，2022年，8月28日文字：

若P是原子，則P,P稱為文字。P稱為正文字，P稱為負文字。子句：

公式P稱為子句，若P為L1…Ln，其中L1,…,Ln是文字。基項、基原子、基子句：沒有變量符號出現的項、原子、子句，分別稱為基項、基原子、基子句。第十三頁，共六十四頁，2022年，8月28日例:gcd(45,b)是基項

father(John,Peter)是基原子father(John,Peter)uncle(John,Peter)是基子句第十四頁，共六十四頁，2022年，8月28日謂詞公式的解釋

設D為謂詞公式P的個體域，若對P中的個體常量、函數和謂詞按照如下規(guī)定賦值：（1）為每個個體常量指派D中的一個元素；（2）為每個n元函數指派一個從Dn到D的映射，其中

Dn={(x1,x2,…,xn)|x1,x2,…,xn

D}（3）為每個n元謂詞指派一個從Dn到{F,T}的映射；則稱這些指派為公式P在D上的一個解釋。第十五頁，共六十四頁，2022年，8月28日永真：如果謂詞公式P，對個體域D上的任何一個解釋都取得真值T，則稱P在D上是永真的。如果P在每個非空個體域上均永真，則稱P永真。第十六頁，共六十四頁，2022年，8月28日永假（不可滿足性）如果謂詞公式P對于個體域D上的所有解釋都取得假值F，則稱P在D上是永假的；如果P在每個非空個體域上均永假，則稱P永假。第十七頁，共六十四頁，2022年，8月28日可滿足的：對于謂詞公式P，如果至少存在一個解釋使得公式P在此解釋下的真值為T，則稱公式P是可滿足的。不可滿足的：對謂詞公式P，如果不存在任何解釋，使得P的取值為T，則稱公式P是不可滿足的。第十八頁，共六十四頁，2022年，8月28日4.2推理相關知識推理：指從已知事實出發(fā)，運用已掌握的知識，推導出其中蘊含的事實性結論或歸納出某些新的結論的過程。推理分類：自然演繹：已知事實推理規(guī)則結論歸結：否定結論前提條件矛盾第十九頁，共六十四頁，2022年，8月28日Skolem化：

公式形式是很多樣的。這就會給機器的形式化處理帶來很大的麻煩。為了便于機器處理，把公式化成統(tǒng)一的標準形式，即SKOLEM標準型。第二十頁，共六十四頁，2022年，8月28日Skolem標準型：

設P是公式，P等價于x1…xnG(x1....xn)，并且G＝G1…Gm，其中G1,…,Gm都是子句，則稱G的子句集S={G1,…,Gm}為公式P的Skolem標準型。第二十一頁，共六十四頁，2022年，8月28日對公式P的SKOLEM化的步驟如下：（1）將P化為前束范式（Q1x1）…（Qnxn）H(x1....xn)其中Q1…Qn是存在量詞或者全稱量詞，H為合取范式的形式,不含→,?；第二十二頁，共六十四頁，2022年，8月28日（2）用如下方法消去存在量詞：i)若Qi是一個存在量詞，并且它的左邊沒有全稱量詞，則用一個H中沒有的常量符號代替H中所有的xi，之后消去（Qixi）

第二十三頁，共六十四頁，2022年，8月28日ii)若Qi是一個存在量詞，并且Qj1,…Qjk是Qi左邊的全稱量詞，則取一個H中沒有的函數k元符號f,用f(xj1,…,xjk)代替xi,之后消去（Qixi）。第二十四頁，共六十四頁，2022年，8月28日公式P經過如上處理，可以化為x1…xn(G1…Gm)的形式，其中G1,…,Gm都是子句。省略全稱量詞，再用“，”取代合取符號，便得到公式P的Skolem標準型{G1,…,Gm}。

第二十五頁，共六十四頁，2022年，8月28日任意公式都有與之相對的子句集。一個公式與它的Skolem標準型未必等值，但在不可滿足的意義上是一致的。第二十六頁，共六十四頁，2022年，8月28日置換：是形如{t1/x1,…,tn/xn}的一個有限集合。其中xi（i=1,…,n）是兩兩不同的變量符號,ti是不同于xi的項。置換作用于表達式：

給定置換={t1/x1,…,tn/xn}和表達式E，E表示將E中出現的每一個xi（i=1,…,n）都替換成ti得到的新表達式。第二十七頁，共六十四頁，2022年，8月28日給定兩個置換={t1/x1,…,tn/xn}

={u1/y1,…,um/ym}將集合{t1/x1,…,tn/xn,u1/y1,…,um/ym}刪去以下元素：

ui/yi，當yi{x1,…,xn}

ti/xi，當ti=xi

得到的新置換表示為·

，稱為和

的復合。第二十八頁，共六十四頁，2022年，8月28日

置換滿足結合律

(·

)·

=·(·

)

置換不滿足交換律

·

·

·=·=第二十九頁，共六十四頁，2022年，8月28日合一置換：

給定表達式E1,…,Ek，若存在置換，使得E1=…=Ek

，則稱是E1,…,Ek的一個合一置換。

第三十頁，共六十四頁，2022年，8月28日

例1：設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)))因為E1=E2，所以是E1與E2的合一置換。第三十一頁，共六十四頁，2022年，8月28日例2，設E1與E2同上，={a/x,f(z)/y}，則E1=g(a,f(z))=E2，所以也是E1與E2的合一置換。顯然比簡單，易證=?，其中={h(u)/z}第三十二頁，共六十四頁，2022年，8月28日

最一般合一置換求法：設有公式：E1=P(x,y,z);E2=

P(x,f(a),g(b))從左至右查找不同的項，構成了不一致集：

D1={y,f(a)}繼續(xù)向右比較又得到一個不一致集：D2={z,g(b)}置換為={f(a)/y,g(b)/z}第三十三頁，共六十四頁，2022年，8月28日

求一般置換算法：令W={E1,E2}令k=0,Wk=W,σk=ε;ε是空置換,表示不作置換。如果Wk只有一個表達式，則算法停止，σk就是所要求的結果.找出Wk的不一致集Dk

。若Dk中存在元素xk和tk

，其中xk是變元，tk是項，且xk不在tk中出現，則：σk+1=σk·{tk/xk}Wk+1=wk{tk/xk}k=k+1然后轉（2）。算法終止，W的一般合一置換不存在。第三十四頁，共六十四頁，2022年，8月28日可以證明，如果E1和E2可合一，則算法必停止于第2步。第三十五頁，共六十四頁，2022年，8月28日4.2Horn邏輯程序人工智能：

知識庫：用于推理的知識

數據庫：事實和論據

推理：對知識和數據的消解，獲得結論第三十六頁，共六十四頁，2022年，8月28日4.2Horn邏輯程序已知的知識表示方法有產生式表示法語義網絡表示法邏輯表示法產生式表示法是一類很重要的方法，知識表示成IF…THEN…的形式。采用產生式方法，可以將規(guī)則與事實以統(tǒng)一的格式表示，即Horn子句。第三十七頁，共六十四頁，2022年，8月28日4.2Horn邏輯程序如果在一個子句中最多含有一個正文字，那么該子句稱為Horn子句。若一個子句集內的子句個數有限且都是Horn子句，那么該子句集稱為一個Horn邏輯程序。第三十八頁，共六十四頁，2022年，8月28日4.2Horn邏輯程序Horn子句可以表示成如下形式：規(guī)則體→規(guī)則頭其中規(guī)則體一般是n個原子的合取，n=0,1,…。規(guī)則頭可以是單個原子，也可以是空。第三十九頁，共六十四頁，2022年，8月28日4.2Horn邏輯程序規(guī)則：規(guī)則體非空且規(guī)則頭非空的子句。例如，

father(z,y),father(y,x)→grandfather(z,x)事實：規(guī)則體空且規(guī)則頭非空的子句。例如，→father(John,Peter)。目標：無規(guī)則頭的子句，例如，grandfather(Smith,Peter)→，即要查詢Smith是否是Peter的祖父？第四十頁，共六十四頁，2022年，8月28日4.2Horn邏輯程序一個Horn邏輯程序是Horn子句的集合，也就是規(guī)則和事實的集合。因此，一個Horn邏輯程序相當于一個知識庫。推理即是通過對一組子句按照一定的方式進行消解最終得到新的公式。第四十一頁，共六十四頁，2022年，8月28日自動推理的過程即給定目標子句，機器按照一定的順序對邏輯程序中的子句進行消解，最后得到目標子句，或者得出目標不可滿足的結論。第四十二頁，共六十四頁，2022年，8月28日命題Horn邏輯的自動推理謂詞Horn邏輯的自動推理第四十三頁，共六十四頁，2022年，8月28日4.3命題Horn邏輯中的自動推理在命題Horn邏輯中，子句之間可以按照如下的方式消解。若有子句S1：A1,…,AnS2：B1,…,Bm

Ai則歸結后的子句為

S3：A1,…,Ai-1,B1,…,Bm,Ai+1,…,An

即利用規(guī)則S2將原目標S1轉化為新目標S3.第四十四頁，共六十四頁，2022年，8月28日4.3命題Horn邏輯中的自動推理基于上述消解方式，求證一個目標S：A1,…,An

需要逐一以S的體中的每一個原子Ai作為新的目標進行求證。A1,…,An也稱為S的子目標。在以一個原子Ai為目標進行求證時，考察子句集內所有頭部是Ai的子句，以此子句的體作為新的目標。第四十五頁，共六十四頁，2022年，8月28日4.3命題Horn邏輯中的自動推理當某個關于A的子句體部的所有原子得到滿足時，直接返回A是正確的，而不用再接著考察頭是A的其他子句。假如對于某個原子A，邏輯程序中所有頭部是A的子句都無法滿足，則得出A無法滿足的結論。第四十六頁，共六十四頁，2022年，8月28日原子A的推理算法TorF(A)如下：TorF(A){i=0;while(i<n)//n是此Horn邏輯程序內子句的個數

{if(第i條規(guī)則的頭部=A)//用第i條規(guī)則考察A{if(第i條規(guī)則的體是空的)thenreturn1;//A是事實

elseif(TorF(A1)=…=TorF(Am)=1)//A1…Am是第i條規(guī)則體內的所有原子thenreturn1;//由i規(guī)則推出原子A的正確}i=i+1;//第i條規(guī)則體內并非所有原子正確，從而需要考察別的規(guī)則

}return0;//考察了所有的規(guī)則，都不能推出A}第四十七頁，共六十四頁，2022年，8月28日4.4謂詞Horn邏輯中的自動推理謂詞Horn邏輯的消解要復雜一些。消解方式如下。若有子句S1：A1,…,An

S2：B1,…,BmB，并且Ai,B具有合一置換，則歸結后的子句為S3：(A1,…,Ai-1,B1,…,Bm,Ai+1,…,An)

與命題Horn邏輯相比，需要考慮項的匹配，即合一問題。第四十八頁，共六十四頁，2022年，8月28日4.4謂詞Horn邏輯中的自動推理基于以上消解方式，求證一個目標S1：A1,…,An

時，要求得出的結果應該是一個置換的集合。集合內的每一個元素i應該使A1i,…,Ani成立。第四十九頁，共六十四頁，2022年，8月28日4.4謂詞Horn邏輯中的自動推理在以一個原子Ai為目標進行考察時，考察每一個頭部是Ai的子句，以此子句的體作為新的目標。返回的不是0（假）或者1（真），而應是一個置換的集合Θ。為此先要給出置換算法Substitution以及求表達式合一算法Unify。第五十頁，共六十四頁，2022年，8月28日

4.4謂詞Horn邏輯中的自動推理將置換作用于表達式e的算法如下Substitution(e,){if(e是常量符號)thenreturne;if(e是變量符號x)then{if(t/x)thenreturntelsereturne;}if(e=f(t1,…,tn))then{t1=Substitution(t1,);…tn=Substitution(tn,)returnf(t1,…,tn)}}第五十一頁，共六十四頁，2022年，8月28日4.4謂詞Horn邏輯中的自動推理對兩個表達式e1，e2作合一的算法如下//算法返回一個合一置換或“無法合一”的信息Unify(e1，e2){=空集；ife1是變量符號xthen={e2/x};elseife2是變量符號xthen={e1/x};elseif(e1是常量而e2不是，或e2是常量而e1不是，或e1，e2是兩個不同的常量)thenreturn“無法合一”else//此時e1，e2形如f(t1,…,tn)和g(s1,…,sm)；f,g為函數符號。第五十二頁，共六十四頁，2022年，8月28日4.4謂詞Horn邏輯中的自動推理

{if(fg)thenreturn“無法合一”;else{

1=Unify(t1，s1);

=?

1;

2=Unify(Substitution(t2,),Substitution(s2,));

=?

2;…

n=Unify(Substitution(tn,)，Substitution(sn,));

=?

n;return;}}}第五十三頁，共六十四頁，2022年，8月28日4.4謂詞Horn邏輯中的自動推理例：Horn邏輯程序（知識庫）如下，father(z,y),father(y,x)→grandfather(z,x)，→father(John,Peter)，→father(Smith,John)。

目標為grandfather(Smith,Peter)→，即查詢Smith是否是Peter的祖父？第五十四頁，共六十四頁，2022年，8月28日4.4謂詞Horn邏輯中的自動推理推理過程如下；1.首先通過合一置換={Peter/x,Smith/z}，將目標與知識庫中第一條規(guī)則的規(guī)則頭匹配，得到新目標

father(Smith,y),father(y,Peter)→2.考察知識庫中第二條和第三條規(guī)則，通過合一置換={John/y}與知識庫中的事實匹配→father(Smith,John),→father(John,Peter)因此查詢目標成立，并且返回置換?={Peter/x,John/y,Smith/z}

第五十五頁，共六十四頁，2022年，8月28日4.4謂詞Horn邏輯中的自動推理考察某個原子A的算法TorF(A)如下

TorF(A)輸入A(s1,…,sn),返回置換數組Θ,其中數組元素Θ[i]是一個置換。第五十六頁，共六十四頁，2022年，8月28日

TorF(A){i=0；

Θ=空集；

while(i<n)//n是此Horn邏輯程序內子句的個數

{if(第i條規(guī)則的頭部=A(t1,…,tn)//t1,..,tn是項) {//用第i條規(guī)則考察A

=Unify(A(t1,…,tn),A(s1,…,sn))；

if=“無法合一”,gotoL1if(第i條規(guī)則的體是空的，即事實) thenΘ=Θ{}；

else{//A1…Am是第i條規(guī)則體內所有原子，m>0//下面i1,i2,…,im初值均為1while(TorF(A1)[i1]!=NULL){1=TorF(A1)[i1];i1=i1＋1;第五十七頁，共六十四頁，2022年，8月28日while(TorF(A21)[i2]!=NULL){…while(TorF(Am

m-1)[im]!=NULL){

m=TorF(A1)[im];

=

?

1?…?

m;Θ=Θ{}；

im＝im

+1;}…}}}}L1 :i