AI04人工智能-自動(dòng)推理

人工智能導(dǎo)論

Introduction

toArtificialIntelligence

第四章史忠植

中國(guó)科學(xué)院計(jì)算技術(shù)研究所/2023/10/20史忠植人工智能導(dǎo)論：自動(dòng)推理1自動(dòng)推理AutomatedReasoning2023/10/20史忠植人工智能導(dǎo)論：自動(dòng)推理2內(nèi)容提要4.1概述4.2三段論推理4.3自然演繹推理

4.4歸結(jié)演繹推理

4.5產(chǎn)生式系統(tǒng)

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

4.4歸結(jié)演繹推理

4.5產(chǎn)生式系統(tǒng)

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

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

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

M—PP—MM—PP—M

S—M

S—M

M—S

M—SS—PS—PS—PS—P2023/10/209史忠植人工智能導(dǎo)論：自動(dòng)推理構(gòu)成三段論推理的三個(gè)性質(zhì)命題，在質(zhì)和量上的不同，就形成了三段論的不同形式，這些不同的形式叫做三段論的式。三段論總是由質(zhì)和量不同的A（全稱(chēng)肯定命題）、E（全稱(chēng)否定命題）、I（特稱(chēng)肯定命題）、O（特稱(chēng)否定命題）四種命題組合而成，任何一個(gè)三段論推理都表現(xiàn)為一定的格和式。A、E、I、O都可以作為大前提、小前提和結(jié)論，其排列組合數(shù)目是：4×4×4=64。這樣，每個(gè)格都有64式，四個(gè)格共有64×4=256式。但大多數(shù)是違反三段論規(guī)則的，是錯(cuò)誤的式或無(wú)效式。三段論的式2023/10/2010史忠植人工智能導(dǎo)論：自動(dòng)推理根據(jù)三段論推理的規(guī)則，就可以確定出各個(gè)格的正確式。四個(gè)格總共有256個(gè)式，其中只有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。上面的各個(gè)式中，凡帶有括號(hào)的式叫做“弱式”，共有五個(gè)弱式。弱式就是指可推出全稱(chēng)結(jié)論但只推出一個(gè)特稱(chēng)結(jié)論的式。如第一格中AII式。我們知道，在第一格中，從AA這兩個(gè)前提可以推出全稱(chēng)結(jié)論A，但得出AAI式卻是一個(gè)特稱(chēng)結(jié)論，因而這個(gè)式就是弱式。例如：所有的植物都是生物；（A）

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

4.4歸結(jié)演繹推理

4.5產(chǎn)生式系統(tǒng)

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

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

Q=>Q

它表示：由P

Q

及P為真，可推出Q

為真。例如，由“如果x

是水果，則x

能吃”及“蘋(píng)果是水果”可推出“蘋(píng)果能吃”的結(jié)論。拒取式推理的一般形式是：

P

Q，~Q=>~P

它表示：由P

Q

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

4.4歸結(jié)演繹推理

4.5產(chǎn)生式系統(tǒng)

4.6小結(jié)歸結(jié)演繹推理歸結(jié)演繹推理本質(zhì)上就是一種反證法，它是在歸結(jié)推理規(guī)則的基礎(chǔ)上實(shí)現(xiàn)的。為了證明一個(gè)命題P恒真，它證明其反命題

P恒假，即不存在使得

P為真的解釋。由于量詞，以及嵌套的函數(shù)符號(hào)，使得謂詞公式往往有無(wú)窮的指派，不可能一一測(cè)試

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

前束范式

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

量詞串

無(wú)量詞公式定理：任何公式G都等價(jià)于一個(gè)前束范式Skolem函數(shù)：存在量詞不出現(xiàn)在全稱(chēng)量詞的轄域內(nèi),此時(shí)只要用一個(gè)新的個(gè)體常量(稱(chēng)為Skolem常量)替換受該存在量詞約束的變?cè)涂上ゴ嬖诹吭~存在量詞位于一個(gè)或多個(gè)全稱(chēng)量詞的轄域內(nèi).此時(shí)需要Skolem函數(shù),該函數(shù)的變?cè)褪怯赡切┤Q(chēng)量詞所約束的全稱(chēng)量詞量化的變量.Skolem函數(shù)所使用的函數(shù)符號(hào)必須是新的.2023/10/20史忠植人工智能導(dǎo)論：自動(dòng)推理18SKOLEM標(biāo)準(zhǔn)型Skolem標(biāo)準(zhǔn)型：沒(méi)有存在量詞的公式。設(shè)G是一階邏輯中的公式，將其化為Skolem標(biāo)準(zhǔn)型，母式M給出的子句集S稱(chēng)為公式G的子句集2023/10/20史忠植人工智能導(dǎo)論：自動(dòng)推理19化為子句集謂詞公式化為子句形的步驟

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

x[~P(x)[y[~P(y)P(f(x,y))]~y[~Q(x,y)P(y)]]](2)減少否定符號(hào)的轄域,把“~”移到緊靠謂詞的位置上~(~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史忠植人工智能導(dǎo)論：自動(dòng)推理20化為子句集(3)變量標(biāo)準(zhǔn)化:重新命名變?cè)?使不同量詞約束的變?cè)胁煌拿?

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史忠植人工智能導(dǎo)論：自動(dòng)推理21化為子句集(5)化為前束形:把所有的全稱(chēng)量詞移到公式的左邊,并使每個(gè)量詞的轄域包含這個(gè)量詞后面公式的整個(gè)部分.即得前束形上例變?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史忠植人工智能導(dǎo)論：自動(dòng)推理22化為子句集(7)消去全稱(chēng)量詞:[[~P(x)~P(y)P(f(x,y))][~P(x)Q(x,g(x))][~P(x)~P(g(x))]](8)消去連結(jié)詞符號(hào)

~P(x)~P(y)P(f(x,y))~P(x)Q(x,g(x))~P(x)~P(g(x))(9)更換變量名稱(chēng):對(duì)變?cè)?使不同子句中的變?cè)煌?~P(x1)~P(y)P(f(x1,y))~P(x2)Q(x2,g(x2))~P(x3)~P(g(x3))2023/10/20史忠植人工智能導(dǎo)論：自動(dòng)推理23化為子句集一個(gè)子句內(nèi)的文字可含有變量,但這些變量總是被理解為全稱(chēng)量詞量化的變量G與其子句集S并不等值.但是在不可滿(mǎn)足的意義下兩者是等價(jià)的.而且G是S的邏輯推論,SG.反過(guò)來(lái)不成立2023/10/20史忠植人工智能導(dǎo)論：自動(dòng)推理24謂詞邏輯的子句形定理:若G是給定的公式,而相應(yīng)的子句集為S,則G是不可滿(mǎn)足的當(dāng)且僅當(dāng)S是不可滿(mǎn)足的推論：設(shè)G=G1…Gn,Si

是Gi的Skolem標(biāo)準(zhǔn)型，令S=Si…Sn，則，G是不可滿(mǎn)足的當(dāng)且僅當(dāng)S是不可滿(mǎn)足的。2023/10/20史忠植人工智能導(dǎo)論：自動(dòng)推理25子句集例對(duì)所有的x,y,z來(lái)說(shuō),如果y是x父親,z是y的父親,則z是x的祖父.又知道每個(gè)人都有父親,試問(wèn)對(duì)某個(gè)人來(lái)說(shuō),誰(shuí)是他的祖父?引入謂詞: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史忠植人工智能導(dǎo)論：自動(dòng)推理26子句集例B:(x)(y)Q(x,y)(要證的結(jié)論)S~B:~Q(x,y)ANS(x)其中ANS(x)是人為增加的,在推理過(guò)程中,ANS(x)變量x同Q(x,y)中的x作同樣的變換,當(dāng)推理結(jié)束的時(shí)候,ANS(x)中的變量x便給出了問(wèn)題的解答。因此:S=SA1SA2

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

置換是形如

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

的一個(gè)有限集.其中vi是變量,而ti是不同于vi的項(xiàng)(常量,變量,函數(shù)),且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史忠植人工智能導(dǎo)論：自動(dòng)推理28置換定義：不含任何元素的置換稱(chēng)為空置換，記為

定義:設(shè)={t1/v1,t2/v2,…,tn/vn}是一個(gè)置換，E是一個(gè)表達(dá)式。將E中出現(xiàn)的每一個(gè)變量符號(hào)vi（1

in）,都用項(xiàng)ti置換，這樣得到的表達(dá)式記為E，稱(chēng)E為E的例。2023/10/20史忠植人工智能導(dǎo)論：自動(dòng)推理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).(同時(shí))2023/10/20史忠植人工智能導(dǎo)論：自動(dòng)推理30置換的復(fù)合（乘積）定義：

設(shè)={t1/x1,t2/x2,…,tn/xn}和

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

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

/x1,t2

/x2,…,tn

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

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

=xi,則刪除ti

=xi所得的置換稱(chēng)為

和的復(fù)合或乘積,記為?

2023/10/20史忠植人工智能導(dǎo)論：自動(dòng)推理31置換的復(fù)合（乘積）例子: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史忠植人工智能導(dǎo)論：自動(dòng)推理32置換的復(fù)合（乘積）定理：設(shè)

和

是兩個(gè)置換,E是表達(dá)式，則E(

)=(E

)

設(shè),,是三個(gè)置換,則有:

置換滿(mǎn)足結(jié)合率:(?)?=?(

?)

置換的交換率不成立

?=?=2023/10/20史忠植人工智能導(dǎo)論：自動(dòng)推理33合一定義:

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

則稱(chēng)E1,...,En是可合一的,并且稱(chēng)為一合一置換.也稱(chēng)為{E1,…,En}的合一子(unifier).定義：如果對(duì){E1,…,En}存在這樣的合一子,則稱(chēng)集合{E1,…,En}是可合一的.2023/10/20史忠植人工智能導(dǎo)論：自動(dòng)推理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史忠植人工智能導(dǎo)論：自動(dòng)推理35最一般合一定義:設(shè)是公式集E的一個(gè)合一,如果對(duì)于任一個(gè)合一,都存在置換使得:=?,則稱(chēng)是公式集E的最一般合一置換,記為mgu(mostgeneralunifier)2023/10/20史忠植人工智能導(dǎo)論：自動(dòng)推理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史忠植人工智能導(dǎo)論：自動(dòng)推理37合一算法(1)令k=0,W0=W(W={E1,E2}),

0=

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

k=mgu

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

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

k+1=

k?{tk/xk}

W

k+1=W

k{tk/xk}=W

k+1(5)k=k+1

然后轉(zhuǎn)(2)2023/10/20史忠植人工智能導(dǎo)論：自動(dòng)推理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史忠植人工智能導(dǎo)論：自動(dòng)推理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史忠植人工智能導(dǎo)論：自動(dòng)推理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)}.不可合一,沒(méi)有mgu.2023/10/20史忠植人工智能導(dǎo)論：自動(dòng)推理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史忠植人工智能導(dǎo)論：自動(dòng)推理42合一算法性質(zhì)：若W是關(guān)于表達(dá)式的有限非空可合一集合，則合一算法將在第（2）步結(jié)束，并且最后的

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

稱(chēng)為C1和C2的一個(gè)二元?dú)w結(jié)式,而L1L2稱(chēng)為被歸結(jié)的文字若R(C1,C2)是C1,C2的二元?dú)w結(jié)式,則:

C1C2

=>R(C1,C2)2023/10/20史忠植人工智能導(dǎo)論：自動(dòng)推理44歸結(jié)式--例子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的二元?dú)w結(jié)式.2023/10/20史忠植人工智能導(dǎo)論：自動(dòng)推理45歸結(jié)式--例子

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史忠植人工智能導(dǎo)論：自動(dòng)推理46歸結(jié)式因子定義

如果一個(gè)子句C的幾個(gè)文字有mgu,則C稱(chēng)為子句C的因子例子

設(shè)C=P(x)P(f(y)~Q(x)假設(shè)={f(y)/x},則:C=P(f(y))~Q(f(y))2023/10/20史忠植人工智能導(dǎo)論：自動(dòng)推理47歸結(jié)式定義:設(shè)C1和C2是無(wú)公共變量的子句,其歸結(jié)式是下列二元?dú)w結(jié)式之一:(1)C1和C2的二元?dú)w結(jié)式(2)C1的因子和C2的二元?dú)w結(jié)式(3)C1和C2的因子的二元?dú)w結(jié)式(4)C1的因子和C2的因子的二元?dú)w結(jié)式該歸結(jié)式仍記為R(C1,C2)2023/10/20史忠植人工智能導(dǎo)論：自動(dòng)推理48歸結(jié)式例: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史忠植人工智能導(dǎo)論：自動(dòng)推理49歸結(jié)反演謂詞邏輯的歸結(jié)反演是僅有一條推理規(guī)則的問(wèn)題求解方法，為證明|-A

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

進(jìn)而得到相應(yīng)的子句集S，只需證明S是不可滿(mǎn)足的即可。

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

Tony、Mike和John都是AlpineClub的會(huì)員。每個(gè)會(huì)員或者是一個(gè)滑雪愛(ài)好者，或者是一個(gè)登山愛(ài)好者，或者都是。沒(méi)有一個(gè)登山愛(ài)好者喜歡下雨，所有的滑雪愛(ài)好者都喜歡雪。Tony喜歡的所有東西Mike都不喜歡，Tony不喜歡的所有東西Mike都喜歡。Tony喜歡雨和雪。用謂詞演算表達(dá)上述信息。把問(wèn)題“誰(shuí)是該俱樂(lè)部的會(huì)員，他是一個(gè)登山愛(ài)好者，但不是滑雪愛(ài)好者”表達(dá)為一個(gè)謂詞表達(dá)式，用歸結(jié)反駁提取答案2023/10/20史忠植人工智能導(dǎo)論：自動(dòng)推理532023