AI04人工智能-自動推理

人工智能導論

Introduction

toArtificialIntelligence

第四章史忠植

中國科學院計算技術研究所/2023/10/20史忠植人工智能導論：自動推理1自動推理AutomatedReasoning2023/10/20史忠植人工智能導論：自動推理2內容提要4.1概述4.2三段論推理4.3自然演繹推理

4.4歸結演繹推理

4.5產生式系統

4.6小結自動推理是人工智能的核心內容之一，是專家系統、程序推導、程序正確性證明、智能機器人等研究領域的重要基礎。自動推理早期的工作主要集中在機器定理證明。1930年希爾伯特（Herbrand）為定理證明建立了一種重要方法，他的方法奠定了機械定理證明的基礎。機械定理證明的主要突破是1965年由魯賓遜做出的，他建立了所謂歸結原理，使機械定理證明達到了應用階段。在本章，首先討論三段論推理，然后討論歸結演繹推理、產生式系統，最后討論非單調推理。自動推理2023/10/203史忠植人工智能導論：自動推理2023/10/20史忠植人工智能導論：自動推理4內容提要4.1概述4.2三段論推理4.3自然演繹推理

4.4歸結演繹推理

4.5產生式系統

4.6小結三段論是一種常用的推理形式，它由三個性質命題組成，其中兩個性質命題是前提，另一個性質命題是結論。例如科學是不斷發(fā)展的；(大前提)

智能科學是科學：(小前提)

所以，智能科學是不斷發(fā)展的。(結論)這就是一個三段論。前兩個性質判斷包含著一個共同項——“科學”，由這兩個具有同項的判斷推出一個新的性質判斷：智能科學是不斷發(fā)展的。三段論2023/10/205史忠植人工智能導論：自動推理其中，結論中的主項叫做小項，用“S”表示，如上例中的“智能科學"；結論中的謂項叫做大項，用“P”表示，如上例中的“不斷發(fā)展的"；兩個前提中共有的項叫做中項，用“M”表示，如上例中的“科學"。在三段論中，含有大項的前提叫大前提，如上例中的“科學是不斷發(fā)展的”；含有小項的前提叫小前提，如上例中的“智能科學是科學"。三段論2023/10/206史忠植人工智能導論：自動推理三段論的公理三段論的公理是三段論推理的基本依據。三段論的公理是客觀事物的最一般、最普遍的關系在人們思維中的反映，是在人類長期反復實踐中被總結出來的，并不斷被實踐所證明的，具有不證自明性。三段論的公理內容：對一類事物的全部有所斷定（肯定或否定），則對該類事物的部分也就有所斷定（肯定或否定）。三段論的公理用圖表示如下：2023/10/207史忠植人工智能導論：自動推理PMSSMP圖1圖2三段論的公理在圖1中，M類全部包含在P類中（所有M是P），S類是M類的一部分（所有S是M），可見，S類的全部必然包含在P類中的。在圖2中，M類全部與P類相排斥（所有M不是P），S類是M類的一部分（所有S是M），可見，S類的全部必然與P類相排斥。2023/10/208史忠植人工智能導論：自動推理三段論的格三段論的格就是根據中項在三段論中的不同位置所構成的不同形式的三段論。在三段論的第一格中，中項是大前提的主項、小前提的謂項；在第二格中，中項是大、小前提的謂項；在第三格中，中項是大、小前提的主項；在第四格中，中項是大前提的謂項、小前提的主項。三段論的四個格可以分別表示如下：第一格第二格第三格第四格

M—PP—MM—PP—M

S—M

S—M

M—S

M—SS—PS—PS—PS—P2023/10/209史忠植人工智能導論：自動推理構成三段論推理的三個性質命題，在質和量上的不同，就形成了三段論的不同形式，這些不同的形式叫做三段論的式。三段論總是由質和量不同的A（全稱肯定命題）、E（全稱否定命題）、I（特稱肯定命題）、O（特稱否定命題）四種命題組合而成，任何一個三段論推理都表現為一定的格和式。A、E、I、O都可以作為大前提、小前提和結論，其排列組合數目是：4×4×4=64。這樣，每個格都有64式，四個格共有64×4=256式。但大多數是違反三段論規(guī)則的，是錯誤的式或無效式。三段論的式2023/10/2010史忠植人工智能導論：自動推理根據三段論推理的規(guī)則，就可以確定出各個格的正確式。四個格總共有256個式，其中只有24式是正確的式。各格正確式如下：第一格：AAA，（AAI），EAE，（EAO），AII，EIO。第二格：AEE，（AEO），EAE，（EAO），AOO，EIO。第三格：AAI，EAO，AII，EIO，IAI，OAO。第四格：AAI，AEE，（AEO），IAI，EAO，EIO。上面的各個式中，凡帶有括號的式叫做“弱式”，共有五個弱式。弱式就是指可推出全稱結論但只推出一個特稱結論的式。如第一格中AII式。我們知道，在第一格中，從AA這兩個前提可以推出全稱結論A，但得出AAI式卻是一個特稱結論，因而這個式就是弱式。例如：所有的植物都是生物；（A）

所有的玫瑰花都是植物；（A）所以，有的玫瑰花是生物。（I）三段論的式2023/10/2011史忠植人工智能導論：自動推理2023/10/20史忠植人工智能導論：自動推理12內容提要4.1概述4.2三段論推理4.3自然演繹推理

4.4歸結演繹推理

4.5產生式系統

4.6小結13自然演繹推理自然演繹推理是從一組已知為真的事實出發(fā)，直接運用經典邏輯的推理規(guī)則，推出結論的過程。其中，基本的推理規(guī)則有P規(guī)則、T

規(guī)則、假言推理、拒取式推理等。P規(guī)則是指在推理的任何步驟上都可以引入前提，繼續(xù)進行推理。T規(guī)則是指在推理時，如果前面步驟中有一個或多個公式永真蘊涵S，則可以把S引入到推理過程中。2023/10/20史忠植人工智能導論：自動推理14自然演繹推理假言推理的一般形式是：P，P

Q=>Q

它表示：由P

Q

及P為真，可推出Q

為真。例如，由“如果x

是水果，則x

能吃”及“蘋果是水果”可推出“蘋果能吃”的結論。拒取式推理的一般形式是：

P

Q，~Q=>~P

它表示：由P

Q

為真及Q為假，可推出P為假。例如，由“如果下雨，則地上濕”及“地上不濕”可推出“沒有下雨”的結論。2023/10/20史忠植人工智能導論：自動推理2023/10/20史忠植人工智能導論：自動推理15內容提要4.1概述4.2三段論推理4.3自然演繹推理

4.4歸結演繹推理

4.5產生式系統

4.6小結歸結演繹推理歸結演繹推理本質上就是一種反證法，它是在歸結推理規(guī)則的基礎上實現的。為了證明一個命題P恒真，它證明其反命題

P恒假，即不存在使得

P為真的解釋。由于量詞，以及嵌套的函數符號，使得謂詞公式往往有無窮的指派，不可能一一測試

P是否為真或假。那么如何來解決這個問題呢？幸運的是存在一個域，即Herbrand域，它是一個可數無窮的集合，如果一個公式基于Herbrand解釋為假，則就在所有的解釋中取假值?；贖erbrand域，希爾伯特（HerbrandD）給出了重要的定理，為不可滿足的公式判定過程奠定了基礎。Robinson給出了用于從不可滿足的公式推出F的歸結推理規(guī)則，為定理機械證明取得了重要的突破，使其達到了應用的階段。2023/10/20史忠植人工智能導論：自動推理16歸結演繹推理歸結證明過程是一種反駁程序，即不是證明一個公式是有效的，而是證明公式之非是不一致的。這完全是為了方便，并且不失一般性。歸結推理規(guī)則所應用的對象是命題或謂詞合式公式的一種特殊的形式，稱為子句。因此在使用歸結推理規(guī)則進行歸結之前需要把合式公式化為子句式。在數理邏輯中，我們知道如何把一個公式化成前束標準型（Q1x1）…（Qnxn）M，由于M中不含量詞總可以把它變換成合取范式。無論是前束標準型還是合取范式都是與原來的合式公式等值的。2023/10/20史忠植人工智能導論：自動推理17SKOLEM標準型

前束范式

(Q1x1)…(Qnxn)M(x1,…,xn)前束形==(前綴){母式}

量詞串

無量詞公式定理：任何公式G都等價于一個前束范式Skolem函數：存在量詞不出現在全稱量詞的轄域內,此時只要用一個新的個體常量(稱為Skolem常量)替換受該存在量詞約束的變元就可消去存在量詞存在量詞位于一個或多個全稱量詞的轄域內.此時需要Skolem函數,該函數的變元就是由那些全稱量詞所約束的全稱量詞量化的變量.Skolem函數所使用的函數符號必須是新的.2023/10/20史忠植人工智能導論：自動推理18SKOLEM標準型Skolem標準型：沒有存在量詞的公式。設G是一階邏輯中的公式，將其化為Skolem標準型，母式M給出的子句集S稱為公式G的子句集2023/10/20史忠植人工智能導論：自動推理19化為子句集謂詞公式化為子句形的步驟

x[P(x)[y[P(y)P(f(x,y))]~y[Q(x,y)P(y)]]](1)消去蘊含符號:PQ~PQ

x[~P(x)[y[~P(y)P(f(x,y))]~y[~Q(x,y)P(y)]]](2)減少否定符號的轄域,把“~”移到緊靠謂詞的位置上~(~P)P~(PQ)~P~Q~(PQ)~P~Q~(x)P(x)~P~(x)P(x)~P

x[~P(x)[y[~P(y)P(f(x,y))]y[Q(x,y)~P(y)]]]2023/10/20史忠植人工智能導論：自動推理20化為子句集(3)變量標準化:重新命名變元名,使不同量詞約束的變元有不同的名字.

x[~P(x)[y[~P(y)P(f(x,y))]w[Q(x,w)~P(w)]]](4)消去存在量詞:

x[~P(x)[y[~P(y)P(f(x,y))][Q(x,g(x))~P(g(x))]]]2023/10/20史忠植人工智能導論：自動推理21化為子句集(5)化為前束形:把所有的全稱量詞移到公式的左邊,并使每個量詞的轄域包含這個量詞后面公式的整個部分.即得前束形上例變?yōu)?

x

y[~P(x)[[~P(y)P(f(x,y))][Q(x,g(x))~P(g(x))]]](6)把母式化為合取范式:上例變?yōu)?

x

y[[~P(x)~P(y)P(f(x,y))] [~P(x)Q(x,g(x))] [~P(x)~P(g(x))]]2023/10/20史忠植人工智能導論：自動推理22化為子句集(7)消去全稱量詞:[[~P(x)~P(y)P(f(x,y))][~P(x)Q(x,g(x))][~P(x)~P(g(x))]](8)消去連結詞符號

~P(x)~P(y)P(f(x,y))~P(x)Q(x,g(x))~P(x)~P(g(x))(9)更換變量名稱:對變元更名,使不同子句中的變元不同名.~P(x1)~P(y)P(f(x1,y))~P(x2)Q(x2,g(x2))~P(x3)~P(g(x3))2023/10/20史忠植人工智能導論：自動推理23化為子句集一個子句內的文字可含有變量,但這些變量總是被理解為全稱量詞量化的變量G與其子句集S并不等值.但是在不可滿足的意義下兩者是等價的.而且G是S的邏輯推論,SG.反過來不成立2023/10/20史忠植人工智能導論：自動推理24謂詞邏輯的子句形定理:若G是給定的公式,而相應的子句集為S,則G是不可滿足的當且僅當S是不可滿足的推論：設G=G1…Gn,Si

是Gi的Skolem標準型，令S=Si…Sn，則，G是不可滿足的當且僅當S是不可滿足的。2023/10/20史忠植人工智能導論：自動推理25子句集例對所有的x,y,z來說,如果y是x父親,z是y的父親,則z是x的祖父.又知道每個人都有父親,試問對某個人來說,誰是他的祖父?引入謂詞:P(x,y):表示x是y的父親Q(x,y):表示x是y的祖父A1:(x)(y)(z)(P(x,y)P(y,z)Q(x,z))SA1:~P(x,y)~P(y,z)Q(x,z)A2:(y)(x)P(x,y)SA2:P(f(y),y)2023/10/20史忠植人工智能導論：自動推理26子句集例B:(x)(y)Q(x,y)(要證的結論)S~B:~Q(x,y)ANS(x)其中ANS(x)是人為增加的,在推理過程中,ANS(x)變量x同Q(x,y)中的x作同樣的變換,當推理結束的時候,ANS(x)中的變量x便給出了問題的解答。因此:S=SA1SA2

S~B2023/10/20史忠植人工智能導論：自動推理27置換和合一置換和合一是為了處理謂詞邏輯中子句之間的模式匹配而引進.定義:

置換是形如

{t1/v1,t2/v2,…,tn/vn}

的一個有限集.其中vi是變量,而ti是不同于vi的項(常量,變量,函數),且vi

vj(i

j)

,

i,j=1,…,n例子：{a/x,w/y,f(s)/z},{g(x)/x}是置換;{x/x},{y/f(x)}不是置換;2023/10/20史忠植人工智能導論：自動推理28置換定義：不含任何元素的置換稱為空置換，記為

定義:設={t1/v1,t2/v2,…,tn/vn}是一個置換，E是一個表達式。將E中出現的每一個變量符號vi（1

in）,都用項ti置換，這樣得到的表達式記為E，稱E為E的例。2023/10/20史忠植人工智能導論：自動推理29置換例子：E=P(x,y,z),={a/x,f(b)/y,c/z}E=P(a,f(b),c)E=P(x,g(y),h(x,z)),={a/x,f(b)/y,g(w)/z}E=P(a,g(f(b)),h(a,g(w)))E=P(x,y,z),={y/x,z/y}E=P(y,z,z).EP(z,z,z).(同時)2023/10/20史忠植人工智能導論：自動推理30置換的復合（乘積）定義：

設={t1/x1,t2/x2,…,tn/xn}和

={u1/y1,u2/y2,…,um/ym}是兩個置換,

也是一個置換,可定義為:先作置換:{t1

/x1,t2

/x2,…,tn

/xn,u1/y1,u2/y2,…,um/ym}若:yi

(x1,x2,…,xn)則刪除ui/yi若:ti

=xi,則刪除ti

=xi所得的置換稱為

和的復合或乘積,記為?

2023/10/20史忠植人工智能導論：自動推理31置換的復合（乘積）例子:E=P(x,y,z)={a/x,f(z)/y,w/z}E=P(a,f(z),w)={t/z,g(b)/w}E=P(a,f(t),g(b))={a/x,f(t)/y,g(b)/z}2023/10/20史忠植人工智能導論：自動推理32置換的復合（乘積）定理：設

和

是兩個置換,E是表達式，則E(

)=(E

)

設,,是三個置換,則有:

置換滿足結合率:(?)?=?(

?)

置換的交換率不成立

?=?=2023/10/20史忠植人工智能導論：自動推理33合一定義:

設有公式集E={E1,...,En}和置換,使得:E1=E2=…=En

則稱E1,...,En是可合一的,并且稱為一合一置換.也稱為{E1,…,En}的合一子(unifier).定義：如果對{E1,…,En}存在這樣的合一子,則稱集合{E1,…,En}是可合一的.2023/10/20史忠植人工智能導論：自動推理34合一例1:E={P(a,y),P(x,f(b))},={a/x,f(b)/y}.E={P(a,b),P(x,f(b))}合一子不一定唯一E={P(a,y),P(x,f(b))}

1={a/x,f(b)/y}(唯一)E={P(x,y),P(x,f(b))}

1={a/x,f(b)/y}(不唯一)

2={b/x,f(b)/y}2023/10/20史忠植人工智能導論：自動推理35最一般合一定義:設是公式集E的一個合一,如果對于任一個合一,都存在置換使得:=?,則稱是公式集E的最一般合一置換,記為mgu(mostgeneralunifier)2023/10/20史忠植人工智能導論：自動推理36最一般合一例子:E={P(x,y),P(x,f(b))}

1={a/x,f(b)/y}

2={b/x,f(b)/y}

={f(b)/y}

1=

{a/x}

2=

{b/x}2023/10/20史忠植人工智能導論：自動推理37合一算法(1)令k=0,W0=W(W={E1,E2}),

0=

(2)如果Wk已經合一,則算法停止,

k=mgu

否則，求出Wk的差異集Dk(3)如果Dk中存在元素xk,

tk,且xk不在tk中出現,則轉(4)；否則不可合一，停止(4)令

k+1=

k?{tk/xk}

W

k+1=W

k{tk/xk}=W

k+1(5)k=k+1

然后轉(2)2023/10/20史忠植人工智能導論：自動推理38合一算法換名:{P(f(x),x),P(x,a)};如果不換名：D={f(x),x}.換名:{P(f(y),y),P(x,a)};mgu:{f(a)/x,a/y}2023/10/20史忠植人工智能導論：自動推理39合一算法求W={P(a,x,f(g(y))),P(z,f(z),f(u))}的mgu.D0={a,z}.

1=

{a/z}={a/z}.W1=W0

1={P(a,x,f(g(y))),P(a,f(a),f(u))}D1={x,f(a)}.

2=

1{f(a)/x}={a/z,f(a)/x}.W2=W1

2={P(a,f(a),f(g(y))),P(a,f(a),f(u))}D2={g(y),u}.

3=

2{g(y)/u}={a/z,f(a)/x,g(y)/u}W3=W2

3={P(a,f(a),f(g(y)))}

3是mgu.2023/10/20史忠植人工智能導論：自動推理40合一算法求W={Q(f(a),g(x)),Q(y,y)}的mgu.D0={f(a),y}.

1=

{f(a)/y}={f(a)/y}.W1=W0

1={Q(f(a),g(x)),Q(f(a),f(a))}D1={g(x),f(a)}.不可合一,沒有mgu.2023/10/20史忠植人工智能導論：自動推理41合一算法求W={P(f(y),y),P(x,a)}的mgu.D0={f(y),x}.

1=

{f(y)/x}={f(y)/x}.W1=W0

1={P(f(y),y),P(f(y),a)}D1={y,a}.

2=

1{a/y}={f(y)/x}{a/y}={f(a)/x,a/y}.W2=W1

2={P(f(a),a)}

2是mgu.2023/10/20史忠植人工智能導論：自動推理42合一算法性質：若W是關于表達式的有限非空可合一集合，則合一算法將在第（2）步結束，并且最后的

k是W的mgu。若一組表達式E1,…,En是可合一的，則它們的mgu除了相差一個改名外，是唯一確定。2023/10/20史忠植人工智能導論：自動推理43歸結式定義:設C1和C2是兩個無公共變量的子句,L1和L2分別是C1和C2的文字,如果L1和~L2有mgu:,則:(C1-{L1})(C2-{L2})

稱為C1和C2的一個二元歸結式,而L1L2稱為被歸結的文字若R(C1,C2)是C1,C2的二元歸結式,則:

C1C2

=>R(C1,C2)2023/10/20史忠植人工智能導論：自動推理44歸結式--例子C1:P(x)Q(x)C2:~P(a)R(x)重命名C2:~P(a)R(y)L1=P(x),L2=~P(a)L1與~L2有mgu={a/x}(C1–L1

)

(C2–L2

)=({P(a),Q(a)}–{P(a)})({~P(a),R(y)}–{~P(a)})={Q(a)}{R(y)}={Q(a),R(y)}Q(a)

R(y)是C1與C2的二元歸結式.2023/10/20史忠植人工智能導論：自動推理45歸結式--例子

C1=P(x)Q(x)

C2=~P(g(y))~Q(b)R(x)

1={g(y)/x}:R(C1,C2)=Q(g(y))~Q(b)R(x)

2={b/x}:R(C1,C2)=~P(g(y))P(b)R(x)2023/10/20史忠植人工智能導論：自動推理46歸結式因子定義

如果一個子句C的幾個文字有mgu,則C稱為子句C的因子例子

設C=P(x)P(f(y)~Q(x)假設={f(y)/x},則:C=P(f(y))~Q(f(y))2023/10/20史忠植人工智能導論：自動推理47歸結式定義:設C1和C2是無公共變量的子句,其歸結式是下列二元歸結式之一:(1)C1和C2的二元歸結式(2)C1的因子和C2的二元歸結式(3)C1和C2的因子的二元歸結式(4)C1的因子和C2的因子的二元歸結式該歸結式仍記為R(C1,C2)2023/10/20史忠植人工智能導論：自動推理48歸結式例:C1=P(x)P(f(y)Q(g(y))C2=~P(f(g(x)))Q(b)

C1的因子為:

={f(y)/x},C1=P(f(y))Q(g(y))則:R(C1,C2)=Q(g(g(x)))Q(b)2023/10/20史忠植人工智能導論：自動推理49歸結反演謂詞邏輯的歸結反演是僅有一條推理規(guī)則的問題求解方法，為證明|-A

B，其中A、B是謂詞公式。使用反演過程，先建立合式公式：

進而得到相應的子句集S，只需證明S是不可滿足的即可。

2023/10/20史忠植人工智能導論：自動推理50歸結反演設E為已知前提的公式集,Q為目標公式(或結論),用歸結反演證明Q為真的步驟為:(1)否定Q得到~Q(2)把~Q加入到公式集E中,得到{E,~Q}(3)把公式集{E,~Q}化為子句集S(4)應用歸結原理對子句集S中的子句進行歸結,并把每次歸結所得的歸結式并入S中.如此反復進行,若出現空子句,則停止歸結,此時就證明了Q為真.2023/10/20史忠植人工智能導論：自動推理51歸結反演已知：求證：2023/10/20史忠植人工智能導論：自動推理52歸結反演給定下面一段話：

Tony、Mike和John都是AlpineClub的會員。每個會員或者是一個滑雪愛好者，或者是一個登山愛好者，或者都是。沒有一個登山愛好者喜歡下雨，所有的滑雪愛好者都喜歡雪。Tony喜歡的所有東西Mike都不喜歡，Tony不喜歡的所有東西Mike都喜歡。Tony喜歡雨和雪。用謂詞演算表達上述信息。把問題“誰是該俱樂部的會員，他是一個登山愛好者，但不是滑雪愛好者”表達為一個謂詞表達式，用歸結反駁提取答案2023/10/20史忠植人工智能導論：自動推理532023