國(guó)考經(jīng)典邏輯推理

國(guó)考經(jīng)典邏輯推理第一頁(yè)，共一百二十七頁(yè)，編輯于2023年，星期五2023/5/261第四章經(jīng)典邏輯推理基本概念命題邏輯的歸結(jié)法子句形Herbrand定理歸結(jié)原理歸結(jié)過(guò)程的策略控制第二頁(yè)，共一百二十七頁(yè)，編輯于2023年，星期五2023/5/262基本概念推理什么是推理：依據(jù)一定的規(guī)則（策略）從已知的事實(shí)推出新事實(shí)（結(jié)論）的過(guò)程稱為推理。第三頁(yè)，共一百二十七頁(yè)，編輯于2023年，星期五2023/5/263基本概念推理推理方式及其分類p.112

演繹推理、歸納推理（完全與否）、默認(rèn)推理確定推理、不確定推理單調(diào)推理、非單調(diào)推理啟發(fā)式推理、非啟發(fā)式推理

…………第四頁(yè)，共一百二十七頁(yè)，編輯于2023年，星期五2023/5/264基本概念推理推理的控制策略，即求解問(wèn)題的策略。有推理方向、搜索策略、沖突消解策略、求解策略及限制策略等。推理方向正向推理：由原始數(shù)據(jù)出發(fā)尋找可用的知識(shí)得出新事實(shí)，如此繼續(xù)直至得到結(jié)論。自底向上（bottom-up），事實(shí)驅(qū)動(dòng)方式。反向推理：先提出假設(shè)，由此出發(fā)，進(jìn)一步尋找支持假設(shè)的證據(jù)，當(dāng)所需證據(jù)與用戶提供原始數(shù)據(jù)相匹配則成功。自頂向下（top-down），目標(biāo)驅(qū)動(dòng)方式。第五頁(yè)，共一百二十七頁(yè)，編輯于2023年，星期五2023/5/265基本概念正向推理過(guò)程規(guī)則集中的規(guī)則與數(shù)據(jù)庫(kù)中的事實(shí)進(jìn)行匹配，得到匹配的規(guī)則集合。從匹配的規(guī)則集合中選擇一條規(guī)則作為使用規(guī)則。執(zhí)行使用規(guī)則的后件。將該使用規(guī)則的后件輸入數(shù)據(jù)庫(kù)。重復(fù)進(jìn)行，直到達(dá)到目標(biāo)。第六頁(yè)，共一百二十七頁(yè)，編輯于2023年，星期五2023/5/266基本概念正向推理算法（產(chǎn)生式系統(tǒng)）斷言一個(gè)事實(shí)使事實(shí)與某個(gè)規(guī)則的前提相匹配完成事實(shí)和前提的合一代換把代換應(yīng)用于規(guī)則的結(jié)論斷言結(jié)果，并把它應(yīng)用于進(jìn)一步的推理重復(fù)1）~5）第七頁(yè)，共一百二十七頁(yè)，編輯于2023年，星期五2023/5/267基本概念正向推理算法流程還有適用知識(shí)輸入信息從KB中選擇合適知識(shí)新結(jié)果存入數(shù)據(jù)庫(kù)進(jìn)行推理無(wú)解退出有適用知識(shí)DB是否有解輸出解結(jié)果是新的YYYYNNNN第八頁(yè)，共一百二十七頁(yè)，編輯于2023年，星期五2023/5/268基本概念設(shè)計(jì)一正向推理系統(tǒng)能用數(shù)據(jù)庫(kù)（黑板）中的事實(shí)去匹配規(guī)則的前提，若匹配不成功，能自動(dòng)地進(jìn)行下一條規(guī)則的匹配，在匹配時(shí)，采用什么策略等問(wèn)題應(yīng)考慮周到。若某條規(guī)則匹配成功了，系統(tǒng)能將此規(guī)則的結(jié)論部分自動(dòng)加入數(shù)據(jù)庫(kù)。能判斷什么時(shí)候結(jié)束推理。能將匹配成功的規(guī)則記錄下來(lái)。第九頁(yè)，共一百二十七頁(yè)，編輯于2023年，星期五2023/5/269基本概念反向推理過(guò)程用規(guī)則集中的規(guī)則后件與目標(biāo)事實(shí)進(jìn)行匹配，得到匹配的規(guī)則集合。從匹配的規(guī)則集合中選擇一條規(guī)則作為使用規(guī)則。把執(zhí)行的使用規(guī)則的前件作為下一個(gè)循環(huán)的目標(biāo)事實(shí)。重復(fù)進(jìn)行，直到達(dá)到目標(biāo)。第十頁(yè)，共一百二十七頁(yè)，編輯于2023年，星期五2023/5/2610基本概念反向推理算法（產(chǎn)生式系統(tǒng)）提出獲取事實(shí)（目標(biāo)）的請(qǐng)求目標(biāo)和任何已知的事實(shí)都不匹配目標(biāo)和一條規(guī)則的結(jié)論匹配進(jìn)行目標(biāo)和結(jié)論的合一代換將代換應(yīng)用于規(guī)則的前提這個(gè)結(jié)論成為系統(tǒng)的新目標(biāo)新目標(biāo)將執(zhí)行動(dòng)作

8)重復(fù)1）~7）匹配知識(shí)庫(kù)中的事實(shí)匹配規(guī)則的結(jié)論，以更進(jìn)一步推理要求用戶回答必要的信息失敗，原目標(biāo)也失敗第十一頁(yè)，共一百二十七頁(yè)，編輯于2023年，星期五2023/5/2611基本概念反向推理算法流程問(wèn)用戶有此證據(jù)找一個(gè)假設(shè)此假設(shè)為真結(jié)束在事實(shí)庫(kù)有證據(jù)還有假設(shè)YYYYNNNN找出結(jié)論部分含此假設(shè)的所有知識(shí)此假設(shè)為假存入事實(shí)庫(kù)選一條知識(shí)讓它的條件作為新假設(shè)第十二頁(yè)，共一百二十七頁(yè)，編輯于2023年，星期五2023/5/2612基本概念設(shè)計(jì)一反向推理系統(tǒng)能根據(jù)用戶要求或情況提出假設(shè)。能驗(yàn)證此假設(shè)是否在數(shù)據(jù)庫(kù)中。能從知識(shí)庫(kù)中將結(jié)論部分包含此假設(shè)的規(guī)則都找出來(lái)。能將找出來(lái)的規(guī)則的前提部分取出并作為新假設(shè)逐條驗(yàn)證。能判斷假設(shè)是否是證據(jù)節(jié)點(diǎn)，若是，能向用戶提出相應(yīng)問(wèn)題并記錄結(jié)果。能將匹配成功的規(guī)則記錄下來(lái)。能判斷何時(shí)應(yīng)結(jié)束推理。第十三頁(yè)，共一百二十七頁(yè)，編輯于2023年，星期五2023/5/2613基本概念推理沖突消解策略1規(guī)則排序：規(guī)則的編排順序就是規(guī)則啟用的優(yōu)先級(jí)。專一性排序：若某一規(guī)則的條件部分規(guī)定的情況比另一條規(guī)則的條件部分所規(guī)定的情況更專門，則這條規(guī)則有較高的優(yōu)先級(jí)。就近排序：把最近使用的規(guī)則放在最優(yōu)先的位置。規(guī)模排序：按規(guī)則條件部分復(fù)雜程度排序，越復(fù)雜越優(yōu)先。第十四頁(yè)，共一百二十七頁(yè)，編輯于2023年，星期五2023/5/2614基本概念推理沖突消解策略2數(shù)據(jù)排序：把規(guī)則條件部分的所有條件項(xiàng)按優(yōu)先級(jí)次序組織，可用知識(shí)的次序由這些知識(shí)所含條件按字典排序方法進(jìn)行選擇。上下文限制：按問(wèn)題求解狀態(tài)或新描述的上下文分塊組織知識(shí)庫(kù)，在某一求解狀態(tài)，只能使用相對(duì)應(yīng)組中的知識(shí)。數(shù)據(jù)冗余限制：若知識(shí)的操作產(chǎn)生上下文冗余項(xiàng)時(shí)，則降低該知識(shí)的優(yōu)先級(jí)。第十五頁(yè)，共一百二十七頁(yè)，編輯于2023年，星期五2023/5/2615基本概念模式匹配（代換與合一）什么叫模式匹配：是指對(duì)兩個(gè)知識(shí)模式（謂詞公式、框架片斷、語(yǔ)義網(wǎng)絡(luò)片斷等）的比較與耦合，即檢查這兩個(gè)知識(shí)模式是否完全一致或近似一致。模式匹配有確定性匹配與不確定性匹配。什么叫合一：一個(gè)表達(dá)式（公式）的項(xiàng)可以是常量、變量或函數(shù)，合一就是尋找項(xiàng)對(duì)變量的代換而使得表達(dá)式（公式）一致的過(guò)程。合一是AI中很重要的過(guò)程。第十六頁(yè)，共一百二十七頁(yè)，編輯于2023年，星期五2023/5/2616基本概念模式匹配（代換與合一）定義4.1代換：有序?qū)Φ募蟂={t1/x1,t2/x2,…,tn/xn}

表示代換。其中ti/xi表示在公式中用ti代替xi

。例：公式P[x,f(y),B]s1={z/x,w/y}則P[z,f(w),B]s2={A/y}則P[x,f(A),B]s3={g(z)/x}則P[g(z),f(y),B]用代換s作用于公式E所得到的式子記為Es

第十七頁(yè)，共一百二十七頁(yè)，編輯于2023年，星期五2023/5/2617基本概念模式匹配（代換與合一）定義4.2代換的復(fù)合：設(shè)有={t1/x1,t2/x2,…,tn/xn}

和={u1/y1,u2/y2,…,un/yn}是兩個(gè)代換。則兩個(gè)代換的復(fù)合也是一個(gè)代換。={t1/x1,t2/x2,…,tn/xn，u1/y1,u2/y2,…,um/ym}

其中

ti

xi

并且

yi{x1,x2,…,xn}

例：

s1={g(x,y)/z,u/w}s2={A/x,B/y,C/w,D/z,w/u}

則s1s2={g(A,B)/z,A/x,B/y,w/u}性質(zhì)：滿足結(jié)合律，而不滿足交換律（1）2=（12），而一般1221

第十八頁(yè)，共一百二十七頁(yè)，編輯于2023年，星期五2023/5/2618基本概念模式匹配（代換與合一）定義4.3可合一：設(shè)有公式集合F={F1,F2,…,Fn},若存在一個(gè)代換使得

F1=F2=…=Fn

，則稱公式集F是可合一的。稱為公式集F的一個(gè)合一。例：F={P[x,f(y),B],P[x,f(B),B]}

則s1={A/x,B/y}是公式集F的一個(gè)合一

s2={B/y}也是公式集F的一個(gè)合一第十九頁(yè)，共一百二十七頁(yè)，編輯于2023年，星期五2023/5/2619基本概念模式匹配（代換與合一）定義4.4最一般合一mgu(MostGeneralUnifier)：設(shè)是公式集F的一個(gè)合一，如果對(duì)任一個(gè)合一都存在一個(gè)代換，使得=則稱是一個(gè)最一般的合一?？梢宰C明mgu是唯一的。求mgu算法第二十頁(yè)，共一百二十七頁(yè)，編輯于2023年，星期五2023/5/2620基本概念求mgu算法（設(shè)公式集為F）：令k=0,Fk=F,k=。是一個(gè)空代換。若Fk只含一個(gè)表達(dá)式，則算法停止，k即為所求的mgu。找出Fk的差異集Dk

。若Dk中存在元素xk和tk

，其中xk是變?cè)?，tk是項(xiàng)，且xk不在tk中出現(xiàn)，則置：k+1=k{tk/xk},Fk+1=Fk{tk/xk},k=k+1,

然后轉(zhuǎn)2）算法終止，F(xiàn)的mgu不存在第二十一頁(yè)，共一百二十七頁(yè)，編輯于2023年，星期五2023/5/2621基本概念求mgu舉例：

F={P[f(x),y,g(y)],P[f(x),z,g(x)]}

k=0,F0=F,0=,D0={y,z}1=0{y/z}={y/z}F1=F0{y/z

}={P[f(x),y,g(y)],P[f(x),y,g(x)]}k=1,D1={y,x},2=1{y/x}={y/z,y/x}F2=F1{y/z,y/x

}={P[f(y),y,g(y)],P[f(y),y,g(y)]}F2只含一個(gè)表達(dá)式，則算法停止，2即為所求的mgu。mgu={y/z,y/x}第二十二頁(yè)，共一百二十七頁(yè)，編輯于2023年，星期五2023/5/2622基本概念歸結(jié)原理由J.A.Robinson由1965年提出。與演繹法完全不同，新的邏輯演算算法。>>>一階邏輯中，至今為止的最有效的半可判定的算法。即，一階邏輯中任意恒真公式，使用歸結(jié)原理，總可以在有限步內(nèi)給以判定。語(yǔ)義網(wǎng)絡(luò)、框架表示、產(chǎn)生式規(guī)則等等都是以推理方法為前提的。即，有了規(guī)則已知條件，順藤摸瓜找到結(jié)果。而歸結(jié)方法是自動(dòng)推理、自動(dòng)推導(dǎo)證明用的。（“數(shù)學(xué)定理機(jī)器證明”）本課程只討論一階謂詞邏輯描述下的歸結(jié)推理方法，不涉及高階謂詞邏輯問(wèn)題。

第二十三頁(yè)，共一百二十七頁(yè)，編輯于2023年，星期五2023/5/2623第四章經(jīng)典邏輯推理基本概念命題邏輯的歸結(jié)法子句形Herbrand定理歸結(jié)原理歸結(jié)過(guò)程的策略控制第二十四頁(yè)，共一百二十七頁(yè)，編輯于2023年，星期五2023/5/2624第四章經(jīng)典邏輯推理基本概念命題邏輯的歸結(jié)法子句形Herbrand定理歸結(jié)原理歸結(jié)過(guò)程的策略控制第二十五頁(yè)，共一百二十七頁(yè)，編輯于2023年，星期五2023/5/2625命題邏輯的歸結(jié)法歸結(jié)反演推理方法基本思想例：

命題：A1、A2、A3

和B求證：A1∧A2∧A3成立，則B成立，即：A1∧A2∧A3→B反證法：證明A1∧A2∧A3∧B是矛盾式（永假式）

歸結(jié)法是以子句集為背景的第二十六頁(yè)，共一百二十七頁(yè)，編輯于2023年，星期五2023/5/2626子句的概念子句與子句集文字：不含任何連接詞的謂詞公式及其否定。子句(定義4.5)

：任何文字的析取式（謂詞的和）。空子句(定義4.6)

：不含任何文字的子句。空子句的不可滿足性：由于空子句不含任何文字，它不能被任何解釋滿足，所以空子句是永假的，不可滿足的。子句集：由子句構(gòu)成的集合。第二十七頁(yè)，共一百二十七頁(yè)，編輯于2023年，星期五2023/5/2627子句的概念建立子句集合取范式：命題、命題和的與，如：

P∧

（P∨Q）∧（

P∨Q）子句集S：合取范式形式下的子命題（元素）的集合例：命題公式：P∧（P∨Q）∧（P∨Q）子句集S：S={P,P∨Q,P∨Q}第二十八頁(yè)，共一百二十七頁(yè)，編輯于2023年，星期五2023/5/2628子句的概念謂詞公式F相對(duì)應(yīng)的子句集S的求?。篎→SKOLEM標(biāo)準(zhǔn)形 →消去全稱變量 →以“，”取代“∧”，并表示為集合形式。第二十九頁(yè)，共一百二十七頁(yè)，編輯于2023年，星期五2023/5/2629命題邏輯的歸結(jié)法歸結(jié)過(guò)程

將命題寫成合取范式求出子句集對(duì)子句集使用歸結(jié)推理規(guī)則歸結(jié)式作為新子句參加歸結(jié)歸結(jié)式為空子句□，S是不可滿足的（矛盾），原命題成立。

（證明完畢）謂詞的歸結(jié)：除了有量詞和函數(shù)以外，其余和命題歸結(jié)過(guò)程一樣。第三十頁(yè)，共一百二十七頁(yè)，編輯于2023年，星期五2023/5/2630第四章經(jīng)典邏輯推理基本概念命題邏輯的歸結(jié)法子句形Herbrand定理歸結(jié)原理歸結(jié)過(guò)程的策略控制第三十一頁(yè)，共一百二十七頁(yè)，編輯于2023年，星期五2023/5/2631第四章經(jīng)典邏輯推理基本概念命題邏輯的歸結(jié)法子句形Herbrand定理歸結(jié)原理歸結(jié)過(guò)程的策略控制第三十二頁(yè)，共一百二十七頁(yè)，編輯于2023年，星期五2023/5/2632子句形—謂詞公式化為子句集步驟1消去蘊(yùn)含符號(hào)PQP∨Q例：(x){P(x){(y)[P(y)P(f(x,y))]∧

(y)[Q(x,y)P(y)]}}第三十三頁(yè)，共一百二十七頁(yè)，編輯于2023年，星期五2023/5/2633子句形—謂詞公式化為子句集步驟1消去蘊(yùn)含符號(hào)PQP∨Q例：(x){P(x){(y)[P(y)P(f(x,y))]∧

(y)[Q(x,y)P(y)]}}(x){P(x)

∨{(y)[P(y)

∨P(f(x,y))]∧

(y)[Q(x,y)

∨P(y)]}}第三十四頁(yè)，共一百二十七頁(yè)，編輯于2023年，星期五2023/5/2634子句形—謂詞公式化為子句集步驟2減少否定符號(hào)的轄域(P)

P(P∧Q)

P∨Q或(P∨Q)

P∧Q(x)P(x)(x)P(x)或(x)P(x)(x)P(x)

例：

(x){P(x)∨{(y)[P(y)∨P(f(x,y))]∧

(y)[Q(x,y)∨P(y)]}}第三十五頁(yè)，共一百二十七頁(yè)，編輯于2023年，星期五2023/5/2635子句形—謂詞公式化為子句集步驟2減少否定符號(hào)的轄域(P)

P(P∧Q)

P∨Q或(P∨Q)

P∧Q(x)P(x)(x)P(x)或(x)P(x)(x)P(x)

例：

(x){P(x)∨{(y)[P(y)∨P(f(x,y))]∧

(y)[Q(x,y)∨P(y)]}}第三十六頁(yè)，共一百二十七頁(yè)，編輯于2023年，星期五2023/5/2636子句形—謂詞公式化為子句集步驟2例：

(x){P(x)∨{(y)[P(y)∨P(f(x,y))]∧

(y)[Q(x,y)∨P(y)]}}(x){P(x)∨{(y)[P(y)∨P(f(x,y))]∧

(y)

[Q(x,y)∨P(y)]}}(x){P(x)∨{(y)[P(y)∨P(f(x,y))]∧

(y)[

Q(x,y)∧

P(y)]}}第三十七頁(yè)，共一百二十七頁(yè)，編輯于2023年，星期五2023/5/2637子句形—謂詞公式化為子句集步驟3變量標(biāo)準(zhǔn)化，即重新命名變?cè)ＷC每個(gè)量詞有其唯一的約束變量。如：(x){P(x)(x)Q(x)}標(biāo)準(zhǔn)化為(x){P(x)(y)Q(y)}

例：

(x){P(x)∨{(y)[P(y)∨P(f(x,y))]∧

(y)[

Q(x,y)∧

P(y)]}}

第三十八頁(yè)，共一百二十七頁(yè)，編輯于2023年，星期五2023/5/2638子句形—謂詞公式化為子句集步驟3變量標(biāo)準(zhǔn)化，即重新命名變?cè)ＷC每個(gè)量詞有其唯一的約束變量。如：(x){P(x)(x)Q(x)}標(biāo)準(zhǔn)化為(x){P(x)(y)Q(y)}

例：

(x){P(x)∨{(y)[P(y)∨P(f(x,y))]∧

(y)[

Q(x,y)∧

P(y)]}}

(x){P(x)∨{(y)[P(y)∨P(f(x,y))]∧

(w)[

Q(x,w)∧

P(w)]}}第三十九頁(yè)，共一百二十七頁(yè)，編輯于2023年，星期五2023/5/2639子句形—謂詞公式化為子句集步驟4消去存在量詞如：(x)P(x,y)用P(A,y)

替換，A為某一常量。如：(y){(x)P(x,y)}引入Skolem函數(shù)g(y)，用(y)

P(g(y),y)

替換例：

(x){P(x)∨{(y)[P(y)∨P(f(x,y))]∧

(w)[

Q(x,w)∧

P(w)]}}第四十頁(yè)，共一百二十七頁(yè)，編輯于2023年，星期五2023/5/2640子句形—謂詞公式化為子句集步驟4消去存在量詞如：(x)P(x,y)用P(A,y)

替換，A為某一常量。如：(y){(x)P(x,y)}引入Skolem函數(shù)g(y)，用(y)

P(g(y),y)

替換例：

(x){P(x)∨{(y)[P(y)∨P(f(x,y))]∧

(w)[

Q(x,w)∧

P(w)]}}

(x){P(x)∨{(y)[P(y)∨P(f(x,y))]∧[

Q(x,g(x))∧

P(g(x))]}}第四十一頁(yè)，共一百二十七頁(yè)，編輯于2023年，星期五2023/5/2641子句形—謂詞公式化為子句集步驟4消去存在量詞

量詞消去原則： 消去存在量詞“”，略去全稱量詞“”。

注意：左邊有全稱量詞的存在量詞，消去時(shí)該變量改寫成為全稱量詞的函數(shù)；如沒(méi)有，改寫成為常量。

第四十二頁(yè)，共一百二十七頁(yè)，編輯于2023年，星期五2023/5/2642子句形—謂詞公式化為子句集步驟5化為前束形如把所有全稱量詞移到公式的左邊，并使得每個(gè)量詞的轄域包含這個(gè)量詞后面公式的整個(gè)部分，所得公式稱為前束形。例：

(x){P(x)∨{(y)[P(y)∨P(f(x,y))]∧[

Q(x,g(x))∧

P(g(x))]}}第四十三頁(yè)，共一百二十七頁(yè)，編輯于2023年，星期五2023/5/2643子句形—謂詞公式化為子句集步驟5化為前束形如把所有全稱量詞移到公式的左邊，并使得每個(gè)量詞的轄域包含這個(gè)量詞后面公式的整個(gè)部分，所得公式稱為前束形。例：

(x){P(x)∨{(y)[P(y)∨P(f(x,y))]∧[

Q(x,g(x))∧

P(g(x))]}}

(x)(y){P(x)∨{

[P(y)∨P(f(x,y))]∧[

Q(x,g(x))∧

P(g(x))]}}第四十四頁(yè)，共一百二十七頁(yè)，編輯于2023年，星期五2023/5/2644子句形—謂詞公式化為子句集步驟6化前束形為SKOLEM標(biāo)準(zhǔn)形前束范式：把所有的量詞都提到前面去，然后消掉所有量詞。

定義：說(shuō)公式A是一個(gè)前束范式，如果A中的一切量詞都位于該公式的最左邊（不含否定詞），且這些量詞的轄域都延伸到公式的末端。SKOLEM標(biāo)準(zhǔn)形==（全稱量詞串）{母式}

母式：子句的合取式第四十五頁(yè)，共一百二十七頁(yè)，編輯于2023年，星期五2023/5/2645子句形—謂詞公式化為子句集步驟6化前束形為SKOLEM標(biāo)準(zhǔn)形反復(fù)利用分配率，把任一個(gè)母式化為合取范式。A∨(B∧

C)

(A∨B)∧(A∨C)

例：(x)(y){P(x)∨{

[P(y)∨P(f(x,y))]∧[

Q(x,g(x))∧

P(g(x))]}}第四十六頁(yè)，共一百二十七頁(yè)，編輯于2023年，星期五2023/5/2646子句形—謂詞公式化為子句集步驟6化前束形為SKOLEM標(biāo)準(zhǔn)形反復(fù)利用分配率，把任一個(gè)母式化為合取范式。A∨(B∧

C)

(A∨B)∧(A∨C)

例：(x)(y){P(x)

∨{

[P(y)∨P(f(x,y))]

∧

[

Q(x,g(x))∧

P(g(x))]}}(x)(y){{P(x)

∨[P(y)∨P(f(x,y))]}∧{P(x)

∨[

Q(x,g(x))∧

P(g(x))]}}第四十七頁(yè)，共一百二十七頁(yè)，編輯于2023年，星期五2023/5/2647子句形—謂詞公式化為子句集步驟6化前束形為SKOLEM標(biāo)準(zhǔn)形反復(fù)利用分配率，把任一個(gè)母式化為合取范式。A∨(B∧

C)

(A∨B)∧(A∨C)

例：(x)(y){P(x)

∨{

[P(y)∨P(f(x,y))]

∧

[

Q(x,g(x))∧

P(g(x))]}}第四十八頁(yè)，共一百二十七頁(yè)，編輯于2023年，星期五2023/5/2648子句形—謂詞公式化為子句集步驟6化前束形為SKOLEM標(biāo)準(zhǔn)形例：(x)(y){P(x)

∨{

[P(y)∨P(f(x,y))]

∧

[

Q(x,g(x))∧

P(g(x))]}}(x)(y){[P(x)∨P(y)∨P(f(x,y))]∧{P(x)

∨[

Q(x,g(x))

∧P(g(x))]}}(x)(y){[P(x)∨P(y)∨P(f(x,y))]∧[P(x)

∨Q(x,g(x))]∧[P(x)

∨

P(g(x))]}第四十九頁(yè)，共一百二十七頁(yè)，編輯于2023年，星期五2023/5/2649子句形—謂詞公式化為子句集步驟7消去全稱量詞例：

(x)(y){[P(x)∨P(y)∨P(f(x,y))]∧[P(x)∨Q(x,g(x))]∧[P(x)∨

P(g(x))]}[P(x)∨P(y)∨P(f(x,y))]∧[P(x)∨Q(x,g(x))]∧[P(x)∨

P(g(x))]第五十頁(yè)，共一百二十七頁(yè)，編輯于2023年，星期五2023/5/2650子句形—謂詞公式化為子句集步驟8對(duì)變?cè)沟靡粋€(gè)變?cè)?hào)不出現(xiàn)在一個(gè)以上的子句中。例：

[P(x)∨P(y)∨P(f(x,y))]∧[P(x)∨Q(x,g(x))]∧[P(x)∨

P(g(x))][P(x)∨P(y)∨P(f(x,y))]∧[P(z)∨Q(z,g(z))]∧[P(w)∨

P(g(w))]第五十一頁(yè)，共一百二十七頁(yè)，編輯于2023年，星期五2023/5/2651子句形—謂詞公式化為子句集步驟9消去合取符號(hào)用子句集代替合取式，即為所求的子句集。例：

[P(x)∨P(y)∨P(f(x,y))]∧[P(z)∨Q(z,g(z))]∧[P(w)∨

P(g(w))]{P(x)∨P(y)∨P(f(x,y))，P(z)∨Q(z,g(z))，P(w)∨

P(g(w))}第五十二頁(yè)，共一百二十七頁(yè)，編輯于2023年，星期五2023/5/2652子句形定理： 謂詞邏輯的任意公式都可以化為與之等價(jià)的前束范式，但其前束范式不唯一。SKOLEM標(biāo)準(zhǔn)形定義： 消去量詞后的謂詞公式。注意：謂詞公式F的SKOLEM標(biāo)準(zhǔn)形同F(xiàn)并不等值。第五十三頁(yè)，共一百二十七頁(yè)，編輯于2023年，星期五2023/5/2653子句形F是不可滿足的S是不可滿足的F與S不等價(jià)，但在不可滿足的意義下是一致的。

定理： 若F是給定的公式，而S是相應(yīng)的子句集，則F是不可滿足的

S是不可滿足的。

注意：F真不一定S真，而S真必有F真。 即：S

F第五十四頁(yè)，共一百二十七頁(yè)，編輯于2023年，星期五2023/5/2654子句形把F的不可滿足判斷S的不可滿足引用Herbrand定理，研究S的不可滿足性。引用Herbrand定理，以說(shuō)明歸結(jié)原理的意義及一個(gè)原理形成的根基與背景

第五十五頁(yè)，共一百二十七頁(yè)，編輯于2023年，星期五2023/5/2655第四章經(jīng)典邏輯推理基本概念命題邏輯的歸結(jié)法子句形Herbrand定理歸結(jié)原理歸結(jié)過(guò)程的策略控制第五十六頁(yè)，共一百二十七頁(yè)，編輯于2023年，星期五2023/5/2656第四章經(jīng)典邏輯推理基本概念命題邏輯的歸結(jié)法子句形Herbrand定理歸結(jié)原理歸結(jié)過(guò)程的策略控制第五十七頁(yè)，共一百二十七頁(yè)，編輯于2023年，星期五2023/5/2657Herbrand定理名詞:

公式F永真:對(duì)于F的所有解釋,F都為真.

公式F永假:沒(méi)有一個(gè)解釋使F為真.問(wèn)題： 要判定一個(gè)子句集是不可滿足的,就是要判定該子句集中的每一個(gè)子句都是不可滿足的;要判定一個(gè)子句是不可滿足的,則需要判定該子句對(duì)任何非空個(gè)體域的任意解釋都是不可滿足的.可見(jiàn),判定子句集的不可滿足性是一件非常困難的工作.

第五十八頁(yè)，共一百二十七頁(yè)，編輯于2023年，星期五2023/5/2658Herbrand定理問(wèn)題： 一階邏輯公式的永真性（永假性）的判定是否能在有限步內(nèi)完成？第五十九頁(yè)，共一百二十七頁(yè)，編輯于2023年，星期五2023/5/2659Herbrand定理1936年圖靈(Turing)和邱吉(Church)互相獨(dú)立地證明了：“沒(méi)有一般的方法使得在有限步內(nèi)判定一階邏輯的公式是否是永真（或永假）。但是如果公式本身是永真（或永假）的，那么就能在有限步內(nèi)判定它是永真（或永假）。對(duì)于非永真（或永假）的公式就不一定能在有限步內(nèi)得到結(jié)論。判定的過(guò)程將可能是不停止的?！?/p>

第六十頁(yè)，共一百二十七頁(yè)，編輯于2023年，星期五2023/5/2660Herbrand定理Herbrand的思想要證明一個(gè)公式是永假的,采用反證法思想,就是尋找一個(gè)已給的公式是真的解釋。然而，如果所給定的公式的確是永假的，就沒(méi)有這樣的解釋存在，并且算法在有限步內(nèi)停止。因?yàn)榱吭~是任意的，所討論的個(gè)體變量域D是任意的，所以解釋的個(gè)數(shù)是無(wú)窮的，不可數(shù)的，要找到所有解釋是不可能的。第六十一頁(yè)，共一百二十七頁(yè)，編輯于2023年，星期五2023/5/2661Herbrand定理Herbrand的思想思想：判斷任何一個(gè)解釋是困難的。所以簡(jiǎn)化討論域，建立一個(gè)比較簡(jiǎn)單、特殊的域，使得只要在這個(gè)論域上，原謂詞公式仍是不可滿足的，即保證不可滿足的性質(zhì)不變。因此引入H域等概念。D域H域H域與D域關(guān)系示意圖第六十二頁(yè)，共一百二十七頁(yè)，編輯于2023年，星期五2023/5/2662Herbrand定理H域H解釋結(jié)論：Herbrand定理第六十三頁(yè)，共一百二十七頁(yè)，編輯于2023年，星期五2023/5/2663Herbrand定理H域H解釋結(jié)論：Herbrand定理第六十四頁(yè)，共一百二十七頁(yè)，編輯于2023年，星期五2023/5/2664Herbrand定理（H域）H域構(gòu)造方法（定義4.7）：設(shè)S為公式F所對(duì)應(yīng)的子句集，則按下述方法構(gòu)造的域H稱為H域。令H0是S中所有個(gè)體常量的集合，若S中不含個(gè)體常量，則令H0={a}，其中a為任一個(gè)體常量。令Hi+1=Hi∪

{S中所有形如f(x1,x2,……,xn)的元素}，其中f(x1,x2,……,xn)是出現(xiàn)在F中任一函數(shù)符號(hào)，i=0,1,2,3,…。

※

例題請(qǐng)參考教科書(shū)P128第六十五頁(yè)，共一百二十七頁(yè)，編輯于2023年，星期五2023/5/2665Herbrand定理（H域）例題1:

S={P(a),P(x)∨P(f(x))},求H域。H0={a}H1={a,f(a)}H2={a,f(a),f(f(a))}H=H0∪H1∪H2∪......={a,f(a),f(f(a)),……}例題2:

S={P(z),

P(x)∨Q(y)},求H域。H0={a}H1={a}H2={a}H=H0∪H1∪H2∪......={a}第六十六頁(yè)，共一百二十七頁(yè)，編輯于2023年，星期五2023/5/2666Herbrand定理（H域）例題3:

S={P(x),Q(y,f(z,b)),R(a)},求H域。H0={a,b}H1={a,b,f(a,b),f(b,b)}H2={a,b,f(a,b),f(b,b),f(f(a,b),b),f(f(b,b),b),……}H=H0∪H1∪H2∪......

={a,b,f(a,b),f(b,b),……}第六十七頁(yè)，共一百二十七頁(yè)，編輯于2023年，星期五2023/5/2667Herbrand定理（H域）幾個(gè)基本概念基子句：用H域中的元素代換子句中的變?cè)玫降淖泳?，即不含變量的子句。基原子：基子句中的謂詞，即沒(méi)有變量出現(xiàn)的原子。原子集A：子句集中所有基原子構(gòu)成的集合。如

A={所有形如P(t1,t2,…tn)的元素}

（其中P(t1,t2,…tn)

是出現(xiàn)于S中的任一謂詞符號(hào)，而t1,t2,…tn

是S的H域的任意元素）

即把H中的東西填到S的謂詞里去。S中的謂詞是有限的，H是可數(shù)的，因此，A也是可數(shù)的。第六十八頁(yè)，共一百二十七頁(yè)，編輯于2023年，星期五2023/5/2668Herbrand定理（H域）原子集舉例:S={P(a),P(x)∨P(f(x))},H={a,f(a),f(f(a)),……}

A={P(a),P(f(a)),P(f(f(a))),……}S={P(z),

P(x)∨Q(y)},H={a}

A={P(a),Q(a)}S={P(x),Q(y,f(z,b)),R(a)},H={a,b,f(a,b),f(a,a),f(b,a),f(b,b),…}

A={P(a),P(b),Q(a,a),Q(a,b),R(a),R(b),……}第六十九頁(yè)，共一百二十七頁(yè)，編輯于2023年，星期五2023/5/2669Herbrand定理（H域）原子集一旦原子集內(nèi)真值確定好（規(guī)定好），則S在H上的真值可確定。S中的謂詞是有限的，可數(shù)的，H域中的元素是可數(shù)的，因此，原子集A中的元素也是可數(shù)的。由此可見(jiàn)，在無(wú)限不可數(shù)的個(gè)體域D上的問(wèn)題轉(zhuǎn)化成為可數(shù)的問(wèn)題。把謂詞公式的不可滿足性討論從D轉(zhuǎn)換到H域，其復(fù)雜程度得到相應(yīng)減少。不可解問(wèn)題變?yōu)榭山鈫?wèn)題。第七十頁(yè)，共一百二十七頁(yè)，編輯于2023年，星期五2023/5/2670Herbrand定理H域H解釋結(jié)論：Herbrand定理第七十一頁(yè)，共一百二十七頁(yè)，編輯于2023年，星期五2023/5/2671Herbrand定理H域H解釋結(jié)論：Herbrand定理第七十二頁(yè)，共一百二十七頁(yè)，編輯于2023年，星期五2023/5/2672Herbrand定理（H解釋）H解釋I（定義4.8）：取一個(gè)值得到一個(gè)結(jié)論解釋I：謂詞公式F在論域D上任何一組真值的指定稱為一個(gè)解釋。公式F的一個(gè)解釋就是公式F在其論域上的一個(gè)實(shí)例化。H解釋：子句集S在其H域上的解釋稱為H解釋。子句集S在H域上的一個(gè)解釋I滿足下列條件：I映射S中所有常量符號(hào)到它們本身。(即原子集)令f是n元函數(shù)，I是f下的一個(gè)指派，即H中的元素到f的一個(gè)映射（函數(shù)值）。簡(jiǎn)單地說(shuō)(P129)，A中的各元素真假組合都是H的解釋。（或真或假只取一個(gè)）第七十三頁(yè)，共一百二十七頁(yè)，編輯于2023年，星期五2023/5/2673Herbrand定理（H解釋）例：子句集S={P(x)∨Q(x),R(f(y))}有

H域H={a,f(a),f(f(a)),……}

原子集A={P(a),Q(a),R(a),P(f(a)),Q(f(a)),R(f(a)),……}

凡是對(duì)A中各元素真假值的一個(gè)具體設(shè)定都是S的一個(gè)H解釋。如

I1*={P(a),Q(a),R(a),Q(f(a)),R(f(a)),……}I2*={P(a),Q(a),R(a),Q(f(a)),R(f(a)),……}I3*={P(a),Q(a),R(a),Q(f(a)),R(f(a)),……}

I1*I2*I3*中出現(xiàn)的P(a)指P(a)取值為T，出現(xiàn)的

P(a)指P(a)取值為F。第七十四頁(yè)，共一百二十七頁(yè)，編輯于2023年，星期五2023/5/2674Herbrand定理（H解釋）I1*I2*I3*中出現(xiàn)的P(a)指P(a)取值為T，出現(xiàn)的

P(a)指P(a)取值為F。顯然在H域上，這樣定義I*下，S的真假值就確定了。如問(wèn)題：對(duì)于所有的解釋，全是假才可判定。因?yàn)樗薪忉尨砹怂械那闆r，如果可以被窮舉，問(wèn)題便可解決。一般來(lái)說(shuō)，一個(gè)子句集的基原子有無(wú)限多個(gè)，它在H域上的解釋也有無(wú)限多個(gè)。

S的不可滿足問(wèn)題

H上的不可滿足問(wèn)題，有Herbrand定理支持。第七十五頁(yè)，共一百二十七頁(yè)，編輯于2023年，星期五2023/5/2675Herbrand定理（H解釋）如下三個(gè)定理保證了歸結(jié)法的正確性：定理1（定理4.2’）

：

設(shè)I是S的論域D上的解釋，存在對(duì)應(yīng)于I的H解釋I*，使得若有S|I=T，必有S|I*=T。定理2（定理4.2）

： 子句集S是不可滿足的，當(dāng)且僅當(dāng)所有的S的H解釋下為假。定理3（定理4.3）

： 子句集S是不可滿足的，當(dāng)且僅當(dāng)對(duì)每一個(gè)解釋I下，至少有S的某個(gè)子句的某個(gè)基例為假。第七十六頁(yè)，共一百二十七頁(yè)，編輯于2023年，星期五2023/5/2676Herbrand定理（H解釋）基例S中某子句中所有變?cè)?hào)均以S的H域中的元素代入時(shí)，所得的基子句C’稱為C的一個(gè)基例。若一個(gè)子句為假，則此解釋為假。一般來(lái)說(shuō)，D是無(wú)窮不可列的，因此，子句集S也是無(wú)窮不可列的。但S確定后H是無(wú)窮可列的。不過(guò)在H上證明S的不可滿足性仍然是不可能的。計(jì)算機(jī)實(shí)現(xiàn)是困難的，提出歸結(jié)原理第七十七頁(yè)，共一百二十七頁(yè)，編輯于2023年，星期五2023/5/2677Herbrand定理H域H解釋結(jié)論：Herbrand定理第七十八頁(yè)，共一百二十七頁(yè)，編輯于2023年，星期五2023/5/2678Herbrand定理H域H解釋結(jié)論：Herbrand定理第七十九頁(yè)，共一百二十七頁(yè)，編輯于2023年，星期五2023/5/2679Herbrand定理（結(jié)論）Herbrand定理：子句集S是不可滿足的，當(dāng)且僅當(dāng)存在不可滿足的S的有限基例集。

第八十頁(yè)，共一百二十七頁(yè)，編輯于2023年，星期五2023/5/2680Herbrand定理（結(jié)論）定理的意義Herbrand定理已將證明問(wèn)題轉(zhuǎn)化成了命題邏輯問(wèn)題。由此定理保證，可以放心的用機(jī)器來(lái)實(shí)現(xiàn)自動(dòng)推理了。（歸結(jié)原理）注意Herbrand定理給出了一階邏輯的半可判定算法，即僅當(dāng)被證明定理是成立時(shí)，使用該算法可以在有限步得證。而當(dāng)被證定理并不成立時(shí)，使用該算法得不出任何結(jié)論。但是

第八十一頁(yè)，共一百二十七頁(yè)，編輯于2023年，星期五2023/5/2681Herbrand定理（結(jié)論）仍存在的問(wèn)題：基例集序列元素的數(shù)目隨子句集的元素?cái)?shù)目成指數(shù)增加。因此，Herbrand定理是30年代提出的，始終沒(méi)有顯著的成績(jī)。直至1965年Robinson提出了歸結(jié)原理，才使得Herbrand定理的光彩得以發(fā)揮。第八十二頁(yè)，共一百二十七頁(yè)，編輯于2023年，星期五2023/5/2682第四章經(jīng)典邏輯推理概述命題邏輯的歸結(jié)法子句形Herbrand定理歸結(jié)原理歸結(jié)過(guò)程的策略控制第八十三頁(yè)，共一百二十七頁(yè)，編輯于2023年，星期五2023/5/2683歸結(jié)原理基本思想通過(guò)歸結(jié)方法不斷擴(kuò)充待判定的子句集，并設(shè)法使其包含指示矛盾的空子句?？兆泳涫遣豢蓾M足（即永假）的子句（P.126），既然子句集中子句間隱含著合取關(guān)系，空子句的出現(xiàn)實(shí)際上判定了子句集的不可滿足。定義4.9：若P是原子謂詞公式，則稱P與P為互補(bǔ)文字。第八十四頁(yè)，共一百二十七頁(yè)，編輯于2023年，星期五2023/5/2684命題邏輯的歸結(jié)法歸結(jié)（定義4.10）

設(shè)有子句C1,C2，如果C1中的文字L1與C2中的文字L2互補(bǔ)，則消除互補(bǔ)對(duì)，余下部分析取求得新子句→得到歸結(jié)式C12

。例：C1

C2

C12

PP∨Q

Q假言推理

P∨QP∨Q

Q∨Q=Q合并

P∨QP∨

Q

Q∨

Q重言式

P∨QP∨

Q

P∨PPP

□或

NIL空子句

P∨QQ∨R

P∨R

三段論第八十五頁(yè)，共一百二十七頁(yè)，編輯于2023年，星期五2023/5/2685命題邏輯的歸結(jié)法歸結(jié)式性質(zhì)定理4.4：兩個(gè)子句C1和C2的歸結(jié)式C12是C1和C2的邏輯推論，即C1∧C2C12（在任一個(gè)使子句C1和C2為真的解釋I下，必有歸結(jié)式C12為真）推論1：子句集S中子句C1和C2的歸結(jié)式為C12，若用C12

代替C1和C2后得到新子句集S1，則S1不可滿足性

S的不可滿足性推論2：子句集S中子句C1和C2的歸結(jié)式為C12，若把C12

加入S中得到新子句集S2，則S2不可滿足性

S的不可滿足性第八十六頁(yè)，共一百二十七頁(yè)，編輯于2023年，星期五2023/5/2686謂詞邏輯的歸結(jié)法歸結(jié)（含有變量子句的歸結(jié)，定義4.11）設(shè)有兩個(gè)沒(méi)有相同變?cè)淖泳銫1,C2，L1是C1中的文字與L2是C2中的文字，若是L1和L2的mgu，則稱C12=(C1

-{L1

})∨

(C2

-{L2

})為子句C1,C2的二元?dú)w結(jié)式。第八十七頁(yè)，共一百二十七頁(yè)，編輯于2023年，星期五2023/5/2687謂詞邏輯的歸結(jié)法例：P[x,f(A)]∨P[x,f(y)]∨Q(y)P[z,f(A)]∨

Q(z)

取L1為P[x,f(A)]，L2為

P[z,f(A)]

則={x/z}得C12=P[x,f(y)]∨Q(y)∨

Q(x)例：P[x,f(A)]∨P[x,f(y)]∨Q(y)P[z,f(A)]∨

Q(z)

取L1為Q(y)，L2為

Q(z)

則={y/z}得C12=P[x,f(A)]∨P[x,f(y)]∨

P[y,f(A)]

可進(jìn)一步歸結(jié)得到

P[x,f(x)]

第八十八頁(yè)，共一百二十七頁(yè)，編輯于2023年，星期五2023/5/2688謂詞邏輯的歸結(jié)法例：P[x,f(A)]∨P[x,f(y)]∨Q(y)P[z,f(A)]∨

Q(x)

修改C2變?cè)?/p>

P[z,f(A)]∨Q(x1)

取L1為P[x,f(A)]，L2為

P[z,f(A)]

則={x/z}得C12=P[x,f(y)]∨Q(y)∨Q(x)

則={x/z}得C12=P[x,f(y)]∨Q(y)∨

Q(x1)第八十九頁(yè)，共一百二十七頁(yè)，編輯于2023年，星期五2023/5/2689歸結(jié)反演歸結(jié)原理正確性的根本在于，找到矛盾可以肯定不真。方法：和命題邏輯一樣。但由于有函數(shù)，所以要考慮合一和置換。第九十頁(yè)，共一百二十七頁(yè)，編輯于2023年，星期五2023/5/2690歸結(jié)反演置換和合一的注意事項(xiàng)：謂詞的一致性，P()與Q()，不可以常量的一致性，P(a,…)與P(b,….)，不可以 變量，P(a,….)與P(x,…)，可以變量與函數(shù)，P(a,x,….)與P(x,f(x),…)，不可以；但P(a,z,…)與P(x,f(y),…)，可以不能同時(shí)消去兩個(gè)互補(bǔ)對(duì)，P∨Q與P∨Q的空，不可以先進(jìn)行內(nèi)部簡(jiǎn)化（置換、合并）第九十一頁(yè)，共一百二十七頁(yè)，編輯于2023年，星期五2023/5/2691歸結(jié)反演—在定理證明中的應(yīng)用歸結(jié)反演的基本思想

目標(biāo)公式被否定并化為子句集，添加到命題公式集中，用歸結(jié)反演應(yīng)用于聯(lián)合集，并力圖推導(dǎo)出一個(gè)空子句（□或NIL）表示產(chǎn)生一個(gè)矛盾，定理得證。第九十二頁(yè)，共一百二十七頁(yè)，編輯于2023年，星期五2023/5/2692歸結(jié)反演—在定理證明中的應(yīng)用歸結(jié)反演的過(guò)程（證明F→Q）(P.133)寫出謂詞關(guān)系公式F（前提）和Q（目標(biāo)、結(jié)論）否定目標(biāo)Q加入公式集F,寫出謂詞表達(dá)式{F,Q}求SKOLEM標(biāo)準(zhǔn)形化為子句集S對(duì)S中可歸結(jié)的子句做歸結(jié)歸結(jié)式仍放入S中，反復(fù)歸結(jié)過(guò)程得到空子句□(NIL)

，得證第九十三頁(yè)，共一百二十七頁(yè)，編輯于2023年，星期五2023/5/2693歸結(jié)反演—在定理證明中的應(yīng)用證明：每個(gè)儲(chǔ)蓄錢的人都獲得利息，若沒(méi)有利息就沒(méi)有人去儲(chǔ)蓄錢。令：S(x,y)表示x儲(chǔ)蓄yM(x)表示x是錢

I(x)表示x是利息E(x,y)表示x獲得y則前提為

(x)[(y)(

S(x,y)∧M(y))(y)(I(y)∧E(x,y))]

結(jié)論為

(x)I(x)(x)(y)(

S(x,y)

M(y))第九十四頁(yè)，共一百二十七頁(yè)，編輯于2023年，星期五2023/5/2694歸結(jié)反演—在定理證明中的應(yīng)用F:

(x)[(y)(

A(x,y)∧B(y))(y)(C(y)∧D(x,y))]

G:

(x)C(x)(x)(y)(

A(x,y)

B(y))F化為子句得

A(x,y)∨

B(y)∨C(f(x))………….(1)

A(x,y)∨

B(y)∨D(x,f(x))………….(2)

G化為子句得

C(z)……….(3)A(a,b)………..(4)B(b)……….(5)第九十五頁(yè)，共一百二十七頁(yè)，編輯于2023年，星期五2023/5/2695歸結(jié)反演—在定理證明中的應(yīng)用A(x,y)∨B(y)∨D(x,f(x))A(x,y)∨B(y)∨C(f(x))C(z)A(a,b)B(b)(1)(2)(3)(4)(5)NIL(8)B(b)∨C(f(a))(6){a/x,b/y}B(b)(7){f(a)/z}第九十六頁(yè)，共一百二十七頁(yè)，編輯于2023年，星期五2023/5/2696歸結(jié)反演—在定理證明中的應(yīng)用歸結(jié)反演基本算法：給定公式F對(duì)應(yīng)的子句集S，求證目標(biāo)公式G成立。①CLAUSES←S∪{G}②UntilNIL是CLAUSES的成員，do：③begin④在子句集CLAUSES中選擇二個(gè)不同的可歸結(jié)的子句Ci,Cj⑤計(jì)算Ci,Cj的歸結(jié)式Cij⑥CLAUSES←將Cij加入到CLAUSES中⑦end說(shuō)明：可歸結(jié)子句的選擇次序可以是任意的。第九十七頁(yè)，共一百二十七頁(yè)，編輯于2023年，星期五2023/5/2697歸結(jié)反演—在定理證明中的應(yīng)用證明：梯形的對(duì)角線與上下底構(gòu)成的內(nèi)錯(cuò)角相等。xvuy梯形上下底平行平行內(nèi)錯(cuò)角相等引入謂詞：T(x,y,u,v)表示xy為上底，uv為下底的梯形。

P(x,y,u,v)表示xy//uv。

E(x,y,z,v,u,w)表示∠x(chóng)yz=∠vuw。第九十八頁(yè)，共一百二十七頁(yè)，編輯于2023年，星期五2023/5/2698歸結(jié)反演—在定理證明中的應(yīng)用問(wèn)題描述：A1:(x)(y)(u)(v)((T(x,y,u,v)P(x,y,u,v))

//上下底平行A2:(x)(y)(u)(v)((P(x,y,u,v)E(x,y,u,v,u,y))

//平行內(nèi)錯(cuò)角相等A3:T(a,b,c,d)

G:E(a,b,d,c,d,b)第九十九頁(yè)，共一百二十七頁(yè)，編輯于2023年，星期五2023/5/2699歸結(jié)反演—在定理證明中的應(yīng)用化為子句：

A1:T(x,y,u,v)∨P(x,y,u,v)A2:P(x,y,u,v)∨E(x,y,u,v,u,y)A3:T(a,b,d,c)

G:E(a,b,d,c,d,b)acdb第一百頁(yè)，共一百二十七頁(yè)，編輯于2023年，星期五2023/5/26100歸結(jié)反演—在定理證明中的應(yīng)用

T(x,y,u,v)∨P(x,y,u,v)

P(x,y,u,v)∨E(x,y,u,v,u,y)T(a,b,d,c)

E(a,b,d,c,d,b)(1)(2)(3)(4)(6)(5)

P(a,b,d,c)

P(a,b,d,c)NIL第一百零一頁(yè)，共一百二十七頁(yè)，編輯于2023年，星期五2023/5/26101歸結(jié)反演—在定理證明中的應(yīng)用證明如下公式G是否為F的邏輯結(jié)論

F:答案:

是第一百零二頁(yè)，共一百二十七頁(yè)，編輯于2023年，星期五2023/5/26102歸結(jié)反演—求解問(wèn)題的答案基于歸結(jié)法的問(wèn)答系統(tǒng)問(wèn)答系統(tǒng)要解決的問(wèn)題形式：有二種類型：直接問(wèn)答：求證當(dāng)x=A時(shí)，G(A)成立。即：真假證明間接問(wèn)答：求證當(dāng)x=？時(shí)，G(x)成立。即：求值證明前面的證明方法都屬于直接問(wèn)答。間接問(wèn)答方法需要采用構(gòu)造方法。第一百零三頁(yè)，共一百二十七頁(yè)，編輯于2023年，星期五2023/5/26103歸結(jié)反演—求解問(wèn)題的答案例題：如果Peter去那兒，則John就去那兒。如果Peter在學(xué)校。問(wèn)題：

John去哪兒？第一百零四頁(yè)，共一百二十七頁(yè)，編輯于2023年，星期五2023/5/26104歸結(jié)反演—求解問(wèn)題的答案解：用謂詞公式表達(dá)所有前提以及結(jié)論。結(jié)論：第一百零五頁(yè)，共一百二十七頁(yè)，編輯于2023年，星期五2023/5/26105歸結(jié)反演—求解問(wèn)題的答案子句集：上面證明了：在給定前提下結(jié)論成立。但是沒(méi)有給出：John在哪兒。解決問(wèn)題的辦法是：第一百零六頁(yè)，共一百二十七頁(yè)，編輯于2023年，星期五2023/5/26106歸結(jié)反演—求解問(wèn)題的答案解決問(wèn)題的辦法：①由目標(biāo)公式的否定與目標(biāo)公式的析取構(gòu)成重言式(G∨G)，將其加入到公式集中，取代原來(lái)公式集中目標(biāo)公式的否定式。②依據(jù)反演樹(shù)的構(gòu)造方法進(jìn)行歸結(jié)，直到得到某個(gè)子句為止。③以該子句作為對(duì)問(wèn)題的回答。第一百零七頁(yè)，共一百二十七頁(yè)，編輯于2023年，星期五2023/5/26107歸結(jié)反演—求解問(wèn)題的答案上例中，用取代答案是：John在學(xué)校。第一百零八頁(yè)，共一百二十七頁(yè)，編輯于2023年，星期五2023/5/26108歸結(jié)反演—求解問(wèn)題的答案求解的過(guò)程(P.136)寫出謂詞關(guān)系公式F（已知前提）求SKOLEM標(biāo)準(zhǔn)形，化為子句集S寫出待求解問(wèn)題的謂詞公式，然后把它否定并與形式謂詞ANSWER構(gòu)成析取式（變?cè)恢拢┌言撐鋈∈交癁樽泳浼⑷氲絊中，得到子句集S’對(duì)S’中可歸結(jié)的子句做歸結(jié)歸結(jié)式仍放入S中，反復(fù)歸結(jié)過(guò)程得到歸結(jié)式ANSWER，則答案就在ANSWER中。問(wèn)題得到解。第一百零九頁(yè)，共一百二十七頁(yè)，編輯于2023年，星期五2023/5/26109歸結(jié)反演—求解問(wèn)題的答案求猴子吃香蕉問(wèn)題的答案：A1(x)(y)(z)(s)(P(x,y,z,s)P(z,y,z,Walk(x,z,s)))(猴子香蕉箱子各在一處…)A2(x)(y)(s)(P(x,y,x,s)P(y,y,y,Carry(x,y,s)))(猴先到箱處搬箱再到香蕉)A3(s)(P(b,b,b,s)R(Climb(s)))(同處,爬)A4P(a,b,c,s)(初始狀態(tài))A5R(s)∨ANS(s)第一百一十頁(yè)，共一百二十七頁(yè)，編輯于2023年，星期五2023/5/26110歸結(jié)反演—求解問(wèn)題的答案化為子句：A1P(x,y,z,s)∨P(z,y,z,Walk(x,z,s))………….(1)A2P(x,y,x,s)∨P(y,y,y,Carry(x,y,s))………….(2)A3P(b,b,b,s)∨R(Climb(s))…………..(3)A4P(a,b,c,s)…………..(4)A5R(s)∨ANS(s)…………..(5)第一百一十一頁(yè)，共一百二十七頁(yè)，編輯于2023年，星期五2023/5/26111歸結(jié)反演—求解問(wèn)題的答案歸結(jié)P(x1,y,z,s3)∨P(z,y,z,Walk(x1,z,s3))(1)P(x,y,x,s2)∨P(y,y,y,Carry(x,y,s2))(2)P(a,b,c,s4)(4)

R(s1)∨ANS(s1)(5)P(b,b,b,s)∨R(Climb(s))(3)P(b,b,b,s)∨ANS(Climb(s))(6)P(x1,b,z,s3)∨ANS(Climb(Carry(z,b,Walk(x1,z,s3))))(8)ANS(Climb(Carry(c,b,Walk(a,c,s4))))(9){Climb(s)/s1}{b/y,Carry(x,b,s2)/s}{z/x,b/y,Walk(x1,z,s3)/s2}{a/x1,c/z,s4/s3}P(x,b,x,s2)∨

ANS(Climb(Car