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

2023/12/251第4章

自動(dòng)推理2023/12/2524.1引言2023/12/253什么是推理推理就是按某種戰(zhàn)略由知判別推出另一判別的思想過(guò)程知判別：包括已掌握的與求解問(wèn)題有關(guān)的知識(shí)及關(guān)于問(wèn)題的知現(xiàn)實(shí)推理的結(jié)論：由知判別推出新判別推理由程序程序?qū)崿F(xiàn)，稱(chēng)為推理機(jī)2023/12/254推理方式及其分類(lèi)1、演繹推理、歸納推理、默許推理推理的根本義務(wù)是從一種判別推出另一種判別按判別推出的途徑來(lái)劃分，可分為演繹推理、歸納推理及默許推理〔1〕演繹推理演繹推理是從全稱(chēng)判別推導(dǎo)出特稱(chēng)判別或單稱(chēng)判別的過(guò)程演繹推理有多種方式，經(jīng)常用的是三段論式三段論式包括大前提：知的普通性知識(shí)或假設(shè)小前提：關(guān)于所研討的詳細(xì)情況或個(gè)別現(xiàn)實(shí)的判別結(jié)論：由大前提推出的適宜于小前提所示情況的新判別2023/12/255推理方式及其分類(lèi)在任何情況下，由演繹推導(dǎo)出的結(jié)論都是蘊(yùn)涵在大前提的普通性知識(shí)中只需大前提和小前提是正確的，那么由它們推出的結(jié)論必然是正確的(2)歸納推理歸納推理是從足夠多的事例中歸納出普通性結(jié)論的推理過(guò)程，是一種從個(gè)別到普通的推理歸納推理：完全歸納推理、不完全歸納推理完全歸納推理是在進(jìn)展歸納時(shí)調(diào)查了相應(yīng)事物的全部對(duì)象，并根據(jù)這些對(duì)象能否都具有某種屬性，從而推出這個(gè)事物能否具有這個(gè)屬性不完全歸納推理是指只調(diào)查了相應(yīng)事物的部分對(duì)象就得出了結(jié)論2023/12/256推理方式及其分類(lèi)枚舉歸納推理：假設(shè)知某類(lèi)事物的有限可數(shù)個(gè)詳細(xì)事物都具有某種屬性，那么可推出該類(lèi)事物都具有此屬性類(lèi)比推理：在兩個(gè)或兩類(lèi)事物有許多屬性都一樣或類(lèi)似的根底上，推出它們?cè)谄渌麑傩陨弦惨粯踊蝾?lèi)似的一種推理(3)默許推理又稱(chēng)缺省推理，它是在知識(shí)不完全的情況下假設(shè)某些條件曾經(jīng)具備所進(jìn)展的推理擺脫了需求知道全部現(xiàn)實(shí)才干進(jìn)展推理的需求，使得在知識(shí)不完全的情況下也能進(jìn)展推理2023/12/257推理方式及其分類(lèi)2、確定性推理、不確定性推理按推理時(shí)所用知識(shí)確實(shí)定性來(lái)劃分，推理可分為確定性推理、不確定性推理確定性推理〔準(zhǔn)確推理〕：推理時(shí)所用的知識(shí)都是準(zhǔn)確的，推出的結(jié)論也是確定的，其真值或者為真，或?yàn)榧伲瑳](méi)有第三種情況出現(xiàn)不確定性推理〔不準(zhǔn)確推理〕：推理時(shí)所用的知識(shí)不都是準(zhǔn)確的，推出的結(jié)論也不完全是一定的，真值位于真與假之間，命題的外延模糊不清2023/12/258推理方式及其分類(lèi)3、單調(diào)推理、非單調(diào)推理按推理過(guò)程中推出的結(jié)論能否單調(diào)地添加，或推出的結(jié)論能否越來(lái)越接近目的，可分為單調(diào)推理和非單調(diào)推理單調(diào)推理：在推理過(guò)程中隨著推理的向前及新知識(shí)的參與，推出的結(jié)論是呈單調(diào)添加的趨勢(shì)，并且越來(lái)越接近最終目的，在推理過(guò)程中不出現(xiàn)反復(fù)的情況非單調(diào)推理：在推理過(guò)程中由于新知識(shí)的參與，不僅沒(méi)有加強(qiáng)已推出的結(jié)論，反而要否認(rèn)它，使得推理退回到前面的某一步，重新開(kāi)場(chǎng)非單調(diào)推理往往在信息不完全或者情況發(fā)生變化時(shí)出現(xiàn)。2023/12/259推理的控制戰(zhàn)略推理過(guò)程是一個(gè)思想過(guò)程，即求解問(wèn)題的過(guò)程推理的控制戰(zhàn)略主要包括推理方向、搜索戰(zhàn)略、沖突消解戰(zhàn)略、求解戰(zhàn)略及限制戰(zhàn)略等1、推理方向推理方向用于確定推理的驅(qū)動(dòng)方式，分為正向推理、逆向推理、混合推理及雙向推理四種知識(shí)庫(kù)綜合數(shù)據(jù)庫(kù)推理機(jī)2023/12/2510推理的控制戰(zhàn)略正向推理正向推理是從初始形狀出發(fā)，運(yùn)用規(guī)那么，到達(dá)目的形狀。又稱(chēng)為數(shù)據(jù)驅(qū)動(dòng)推理、前向鏈推理、方式制導(dǎo)推理及前件推理。逆向推理逆向推理是以某個(gè)假設(shè)目的為出發(fā)點(diǎn)的一種推理，又稱(chēng)為目的驅(qū)動(dòng)推理、逆向鏈推理、目的制導(dǎo)推理及后件推理2023/12/2511正、逆向推理比較

項(xiàng)目正向推理逆向推理驅(qū)動(dòng)方式數(shù)據(jù)驅(qū)動(dòng)目標(biāo)驅(qū)動(dòng)推理方法從一組數(shù)據(jù)出發(fā)向前推導(dǎo)結(jié)論從可能的解出發(fā)向后推理驗(yàn)證解答啟動(dòng)方法從一個(gè)事件啟動(dòng)由詢(xún)問(wèn)關(guān)于目標(biāo)狀態(tài)的一個(gè)問(wèn)題啟動(dòng)透明程度不能解釋其推理過(guò)程可解釋其推理過(guò)程推理方向由底向上推理由頂向下推理典型系統(tǒng)CLIPS，OPSPROLOG2023/12/2512推理的控制戰(zhàn)略混合推理知的現(xiàn)實(shí)不充分。經(jīng)過(guò)正向推理先把其運(yùn)用條件不能完全匹配的知識(shí)都找出來(lái)，并把這些知識(shí)可導(dǎo)出的結(jié)論作為假設(shè)，然后分別對(duì)這些假設(shè)進(jìn)展逆向推理由正向推理推出的結(jié)論可信度不高希望得到更多的結(jié)論推理的方式：先正向再逆向，經(jīng)過(guò)正向推理，即從知現(xiàn)實(shí)演繹出部分結(jié)果，然后再用逆向推理證明該目的或提高其可信度先逆向再正向，先假設(shè)一個(gè)目的進(jìn)展逆向推理，然后再利用逆向推理中得到的信息進(jìn)展正向推理，以推出更多的結(jié)論2023/12/2513推理的控制戰(zhàn)略雙向推理雙向推理是指正向推理與逆向推理同時(shí)進(jìn)展，且在推理過(guò)程中的某一步驟上“碰頭〞的一種推理。正向推理所得的中間結(jié)論恰好是逆向推理此時(shí)要求的證據(jù)2、求解戰(zhàn)略推理是只求一個(gè)解還是求一切解以及最優(yōu)解等3、限制戰(zhàn)略對(duì)推理的深度、寬度、時(shí)間、空間等進(jìn)展限制2023/12/2514推理的控制戰(zhàn)略4、沖突消解戰(zhàn)略在推理過(guò)程中，匹配會(huì)出現(xiàn)三種情況知現(xiàn)實(shí)不能與知識(shí)庫(kù)中的任何知識(shí)匹配勝利知現(xiàn)實(shí)恰好只與知識(shí)庫(kù)中的一個(gè)知識(shí)匹配勝利知現(xiàn)實(shí)可與知識(shí)庫(kù)中的多個(gè)知識(shí)匹配勝利；或者有多個(gè)〔組〕知現(xiàn)實(shí)都可與知識(shí)庫(kù)中某一知識(shí)匹配勝利；或者有多個(gè)〔組〕知現(xiàn)實(shí)可與知識(shí)庫(kù)中的多個(gè)知識(shí)匹配勝利出現(xiàn)沖突的情況對(duì)正向推理而言，假設(shè)有多條產(chǎn)生式規(guī)那么的前件都和知的現(xiàn)實(shí)匹配勝利；或者有多組不同的知現(xiàn)實(shí)都與同一條產(chǎn)生式規(guī)那么的前件匹配勝利；或者兩種情況同時(shí)出現(xiàn)2023/12/2515推理的控制戰(zhàn)略對(duì)逆向推理而言，假設(shè)有多條產(chǎn)生式的后件都和同一假設(shè)匹配勝利，或者有多條產(chǎn)生式后件可與多個(gè)假設(shè)匹配勝利。按就近原那么排序該戰(zhàn)略把最近被運(yùn)用過(guò)的規(guī)那么賦予較高的優(yōu)先級(jí)。按知現(xiàn)實(shí)的新穎性排序普通我們以為新穎現(xiàn)實(shí)是對(duì)舊知識(shí)的更新和改良，比老知識(shí)更有效，即后生成的現(xiàn)實(shí)比先生成的現(xiàn)實(shí)具有較大的優(yōu)先性。2023/12/2516推理的控制戰(zhàn)略按匹配度排序在不確定推理時(shí)，匹配度不僅可確定兩個(gè)知識(shí)方式能否可匹配，還可用于沖突消解。根據(jù)匹配程度來(lái)決議哪一個(gè)產(chǎn)生式規(guī)那么優(yōu)先被運(yùn)用。按領(lǐng)域問(wèn)題特點(diǎn)排序該方法按照求解問(wèn)題領(lǐng)域的特點(diǎn)將知識(shí)排成固定的次序。按上下文限制排序該戰(zhàn)略將知識(shí)按照所描畫(huà)的上下文分成假設(shè)干組，在推理過(guò)程中根據(jù)當(dāng)前數(shù)據(jù)庫(kù)中的知現(xiàn)實(shí)與上下文的匹配情況，確定選擇某組中的某條知識(shí)。2023/12/2517推理的控制戰(zhàn)略按條件個(gè)數(shù)排序多條規(guī)那么生成的結(jié)論一樣的情況下，由于條件個(gè)數(shù)較少的規(guī)那么匹配所破費(fèi)的時(shí)間較少而且容易實(shí)現(xiàn)，所以將條件少的規(guī)那么賦予較高的優(yōu)先級(jí)，優(yōu)先被啟用。按規(guī)那么的次序排序該戰(zhàn)略是以知識(shí)庫(kù)中預(yù)先存入規(guī)那么的陳列順序作為知識(shí)排序的根據(jù)，排在前面的規(guī)那么具有較高的優(yōu)先級(jí)。2023/12/25184.3自然演繹推理2023/12/2519自然演繹推理的根本概念定義：自然演繹推理是指從一組知的現(xiàn)實(shí)出發(fā)，直接運(yùn)用命題邏輯或謂詞邏輯中的推理規(guī)那么推出結(jié)論的過(guò)程。推理規(guī)那么：P規(guī)那么：在推理的任何步驟上都可引入前提，繼續(xù)進(jìn)展推理。T規(guī)那么：推理時(shí)，假設(shè)前面步驟中有一個(gè)或多個(gè)公式永真蘊(yùn)涵公式S，那么可把S引入推理過(guò)程中。反證法：，當(dāng)且僅當(dāng)。即：Q為P的邏輯結(jié)論，當(dāng)且僅當(dāng)是不可滿(mǎn)足的。2023/12/2520自然演繹推理的根本概念假言推理表示：由及P為真，可推出Q為真

拒取式推理表示：由為真及Q為假，可推出P為假

2023/12/2521自然演繹推理的根本概念一定后件(Q)的錯(cuò)誤：當(dāng)P→Q為真時(shí),希望經(jīng)過(guò)一定后件Q推出前件P為真,這是不允許的.否認(rèn)前件(P)的錯(cuò)誤：當(dāng)P→Q為真時(shí),希望經(jīng)過(guò)否認(rèn)前件P推出后件Q為假,這也是不允許的.防止產(chǎn)生兩類(lèi)錯(cuò)誤：2023/12/2522自然演繹推理的根本概念假設(shè)行星系統(tǒng)是以太陽(yáng)為中心的,那么金星會(huì)顯示出位相變化。金星會(huì)顯示出位相變化。所以，行星系統(tǒng)是以太陽(yáng)為中心的。如伽利略在論證哥白尼的日心說(shuō)時(shí),曾運(yùn)用了以下推理：這就是運(yùn)用了一定后件的推理，違反了經(jīng)典邏輯的邏輯規(guī)那么,他為此曾遭到非難。2023/12/2523自然演繹推理的根本概念假設(shè)上網(wǎng)，那么能知道新聞。沒(méi)有上網(wǎng)。所以，不知道新聞。又如以下推理：這就是運(yùn)用了否認(rèn)前件的推理,違反了邏輯規(guī)那么,顯然是不正確的,由于經(jīng)過(guò)收聽(tīng)廣播、看電視等，也會(huì)知道新聞。2023/12/2524自然演繹推理的優(yōu)缺陷優(yōu)點(diǎn)：定理證明過(guò)程自然，容易了解，而且它擁有豐富的推理規(guī)那么，推理過(guò)程靈敏，便于在它的推理規(guī)那么中嵌入領(lǐng)域啟發(fā)式知識(shí)。缺陷：容易產(chǎn)生組合爆炸，推理過(guò)程中得到的中間結(jié)論普通呈指數(shù)方式遞增。2023/12/2525人的問(wèn)題求解行為更像是一個(gè)解答識(shí)別過(guò)程而非解答搜索過(guò)程識(shí)別解答或部分解答依賴(lài)于運(yùn)用領(lǐng)域特有的知識(shí)，符號(hào)推理那么成為基于知識(shí)來(lái)求解問(wèn)題的主要手段。符號(hào)推理的重要方式是演繹推理它的根底為謂詞演算——一種方式言語(yǔ)將各種陳說(shuō)性〔闡明性〕的描畫(huà)以方式化的方式表示，以便對(duì)它們作處置。謂詞演算——人工智能系統(tǒng)最常用的知識(shí)表示方法，廣泛地運(yùn)用于各種人工智能系統(tǒng)的設(shè)計(jì)。謂詞演算〔或更廣義地，方式邏輯〕是人工智能研討的重要根底之一。主要內(nèi)容：謂詞演算H域和海伯倫定理歸結(jié)原理歸結(jié)反演歸結(jié)演繹推理★2023/12/2526回想謂詞邏輯表示法1、謂詞公式“謂詞公式〞的普通方式：P(x1,x2,…,xn)，其中，P——謂詞符號(hào)〔簡(jiǎn)稱(chēng)謂詞〕；Xi(i=1,2,…,n)——參數(shù)項(xiàng)〔簡(jiǎn)稱(chēng)項(xiàng)〕，項(xiàng)可以是常量、變量或函數(shù)；P(x1,x2,…,xn)——n元謂詞公式；“謂詞公式〞的根本組成：謂詞符號(hào)、常量符號(hào)、變量符號(hào)、函數(shù)符號(hào)；用括號(hào)和逗號(hào)隔開(kāi)，表示論域內(nèi)的關(guān)系。“謂詞公式是謂詞邏輯的根本單元，也稱(chēng)為原子公式。2023/12/25272、連詞和量詞經(jīng)過(guò)引入連詞和量詞，可以把謂詞公式〔原子公式〕組合為復(fù)合謂詞公式。復(fù)合謂詞公式也稱(chēng)為邏輯語(yǔ)句?！?〕連詞〔非〕加在謂詞公式前面，稱(chēng)為否認(rèn)，或取反。〔與〕銜接謂詞公式，稱(chēng)為合取；產(chǎn)生的邏輯語(yǔ)句稱(chēng)為合取式，每個(gè)成分成為合取項(xiàng)?！不颉炽暯又^詞公式，稱(chēng)為析?。划a(chǎn)生的邏輯語(yǔ)句稱(chēng)為析取式，每個(gè)成分成為析取項(xiàng)?！蔡N(yùn)涵〕銜接謂詞公式產(chǎn)生蘊(yùn)涵式；左部稱(chēng)為前項(xiàng)，右部稱(chēng)為后項(xiàng)?！驳葍r(jià)〕銜接謂詞公式產(chǎn)生等價(jià)式；正、逆向蘊(yùn)涵式的合取。2023/12/25282、連詞和量詞經(jīng)過(guò)引入連詞和量詞，可以把原子公式組合為復(fù)合謂詞公式。復(fù)合謂詞公式也稱(chēng)為邏輯語(yǔ)句。〔1〕連詞經(jīng)過(guò)連詞產(chǎn)生的復(fù)合謂詞公式〔邏輯語(yǔ)句〕的真值表：PQPP∧QP∨QPQPQTTFTTTTFTTFTTFTFFFTFFFFTFFTT2023/12/25292、連詞和量詞命題——不包含變量的謂詞公式和邏輯語(yǔ)句；命題邏輯——基于命題的謂詞邏輯稱(chēng)為命題邏輯，命題邏輯是謂詞邏輯的子集。命題邏輯缺乏有效的表達(dá)普通性概念的才干無(wú)法把每個(gè)知識(shí)單元籠統(tǒng)、細(xì)分；如，“條條大路通羅馬〞。Lead(Road1,Roma)Lead(Road2,Roma)……謂詞邏輯中引入變量和對(duì)變量進(jìn)展約束的量詞。〔2〕量詞全稱(chēng)量詞 存在量詞2023/12/25302、連詞和量詞——〔2〕量詞全稱(chēng)量詞符號(hào)(x)P(x)：表示對(duì)于某個(gè)論域中的一切〔恣意一個(gè)〕個(gè)體x,都有P(x)真值為T(mén)。存在量詞符號(hào)(x)P(x)：來(lái)表示某個(gè)論域中至少存在一個(gè)個(gè)體x，使P(x)真值為T(mén)。條條大路通羅馬Mary給每個(gè)人一本書(shū)Mary給每人某個(gè)同樣的東西量詞可以嵌套運(yùn)用可以有不受量詞約束的變量2023/12/25312、連詞和量詞——〔2〕量詞全稱(chēng)量詞符號(hào)(x)P(x)：表示對(duì)于某個(gè)論域中的一切〔恣意一個(gè)〕個(gè)體x,都有P(x)真值為T(mén)。存在量詞符號(hào)(x)P(x)：來(lái)表示某個(gè)論域中至少存在一個(gè)個(gè)體x，使P(x)真值為T(mén)。條條大路通羅馬一切機(jī)器人都是灰色的2023/12/2532一階謂詞邏輯定義：假設(shè)限定不允許對(duì)謂詞和函數(shù)名進(jìn)展量化處置，且參數(shù)項(xiàng)不能是謂詞公式，那么這樣的謂詞邏輯是一階的。謂詞、函數(shù)名的出現(xiàn)位置不允許運(yùn)用變量；參數(shù)項(xiàng)不能是謂詞公式；(P)P(A)-謂詞進(jìn)展了量化；(y)Married(y(L1),Mary)-函數(shù)名進(jìn)展了量化；P(x,Q(y))-參數(shù)項(xiàng)是謂詞公式；2023/12/2533適宜(式)公式1、適宜公式的定義適宜公式適宜于一階謂詞邏輯服從以下遞歸方式定義的邏輯語(yǔ)句稱(chēng)為適宜公式①單一謂詞公式是適宜公式；②假設(shè)A是適宜公式，那么A也是適宜公式；③假設(shè)A和B都是適宜公式，那么A∧B、A∨B、AB和AB也都是適宜公式；④假設(shè)A是適宜公式，x是約束變量，那么(x)A和(x)A也都是適宜公式；⑤只需按上述規(guī)那么①-④求得的公式，才是適宜公式。連詞優(yōu)先級(jí)別是，∧、∨，、，但可經(jīng)過(guò)括號(hào)改動(dòng)優(yōu)先級(jí)。2023/12/2534適宜公式的性質(zhì)適宜公式等價(jià)關(guān)系:否認(rèn)之否認(rèn)

?(?P)P蘊(yùn)涵式轉(zhuǎn)化PQ?P∨Q狄摩根定律

?(P∨Q)?P∧?Q

?(P∧Q)?P∨?Q分配律P∧(Q∨R)(P∧Q)∨(P∧R〕

P∨(Q∧R)(P∨Q)∧(P∨R)5.交換律P∨QQ∨P

P∧QQ∧P2023/12/2535適宜公式的性質(zhì)6.結(jié)合律(P∧Q)∧RP∧(Q∧R〕

(P∨Q)∨RP∨〔Q∨R〕7.逆否律

PQ?Q?P8.量詞否認(rèn)?($x)P(x)(x)(?P(x))

?(x)P(x)〔x)(?P(x))

2023/12/2536適宜公式的性質(zhì)9.量詞分配(x)[P(x)∧Q(x)](x)P(x)∧(x)Q(x)

(x〕[P(x)∨Q(x)]〔x〕P(x)∨(x)Q(x)10.約束變量的虛元性(x)P(x)(y)P(y)

(x)P(x)(y)P(y)(x)[P(x)∧Q(x)](x)P(x)∧(y)Q(y)(x)[P(x)∨Q(x)](x)P(x)∨(y)Q(y)2023/12/2537適宜公式的規(guī)范化★1、規(guī)范化需求常見(jiàn)的基于謂詞演算的推理：歸結(jié)反演、(正向/逆向)歸結(jié)演繹推理要求以量詞前束范式來(lái)表示適宜公式量詞前束范式方式如下：(Q1x1)(Q2x2)…(Qkxk)M，其中M——母式，不包括任何量詞；Qixi——Qi可以是量詞符號(hào)或；xi是量詞的約束變量(i=1,2,…,k)2023/12/2538前束范式例1：變公式〔x〕P〔x〕=>〔x〕Q〔x〕為前束范式~〔x〕P〔x〕∨〔x〕Q〔x〕〔x〕〔~P〔x〕〕∨〔x〕Q〔x〕〔x〕〔~P〔x〕∨Q〔x〕〕為前束范式2023/12/2539前束范式例2：(x)(y){((z)(P(x，z)∧P(y，z))=>(u)Q(x，y，u))}x)(y)(~((z)(P(x，z)∧P(y，z)))∨(u)Q(x，y，u))(x)(y)(z)(~P(x，z)∨~P(y，z))∨(u)Q(x，y，u)x)(y)(z)(u)(~P(x，z)∨~P(y，z)∨Q(x，y，u))2023/12/2540史柯倫規(guī)范型及其構(gòu)造思想史柯倫〔Skolem〕規(guī)范型：海伯倫〔Herbrand〕定理是歸結(jié)原理的根底。海伯倫定理證明的步驟實(shí)踐上是反演法，即不是證明一個(gè)公式是永真，而是證明該公式能否是永假的。反演法利用了一個(gè)規(guī)范型，這個(gè)規(guī)范型就是Skolem規(guī)范型。2023/12/2541一階邏輯公式所對(duì)應(yīng)的Skolem規(guī)范型基于如下思想來(lái)構(gòu)造：一階邏輯的一個(gè)公式被變換為前束范式。其中前束是一個(gè)存在量詞或全稱(chēng)量詞的序列，母式中不在含有量詞。由于母式不含量詞，所以可以變換為合取范式。經(jīng)過(guò)運(yùn)用Skolem函數(shù)，可以在前束中將存在量詞消去，而不影響公式的永假性。2023/12/2542Skolem規(guī)范型經(jīng)過(guò)變換消去存在量詞所得到的公式稱(chēng)為Skolem規(guī)范型，而拿來(lái)替代存在量詞的變量的函數(shù)稱(chēng)Skolem函數(shù)。無(wú)參Skolem函數(shù)有時(shí)稱(chēng)Skolem常量。

從一階邏輯的公式變換到Skolem規(guī)范型不是等值變換，由于Skolem規(guī)范型與原公式不等值。但它們堅(jiān)持永假性。2023/12/2543適宜公式的規(guī)范化★1、規(guī)范化需求常見(jiàn)的基于謂詞演算的推理：歸結(jié)反演、(正向/逆向)演繹推理要求以量詞前束范式來(lái)表示適宜公式量詞前束范式方式如下：(Q1x1)(Q2x2)…(Qkxk)M，其中M——母式，不包括任何量詞；Qixi——Qi可以是量詞符號(hào)或；xi是量詞的約束變量(i=1,2,…,k)歸結(jié)反演——要求M規(guī)范化為合取范式，定義如下：M=W1∧W2∧…∧WnWi=Li1∨Li2∨…∨Lim(i=1,2,…,n)Lij=Pij|Pij:文字〔Literal〕，是謂詞公式Pij或其取反2023/12/25442、合取范式的規(guī)范化過(guò)程運(yùn)用適宜公式性質(zhì)將公式逐漸轉(zhuǎn)化的過(guò)程。轉(zhuǎn)化步驟沒(méi)有嚴(yán)厲的規(guī)定較合理的化簡(jiǎn)過(guò)程，分為8步：①消去多余的量詞〔很少出現(xiàn)〕；②消去蘊(yùn)涵符號(hào)；③減少否認(rèn)的轄域〔內(nèi)移否認(rèn)符號(hào)〕；④變量規(guī)范化〔變量換名〕；⑤消去存在量詞(Skolem變換)；⑥全稱(chēng)量詞前束化〔化為前束形〕；⑦消去全稱(chēng)量詞；⑧把母式轉(zhuǎn)化為合取范式。2023/12/25452、合取范式的規(guī)范化過(guò)程①消去多余的量詞〔很少出現(xiàn)〕假設(shè)一個(gè)量詞的轄域內(nèi)并未出現(xiàn)量詞的約束變量，那么該量詞是多余的，應(yīng)該刪除；例，(x)P(y)，那么(x)可以消去，得到P(y)；正常情況下，適宜公式中不應(yīng)出現(xiàn)多余的量詞。②消去蘊(yùn)涵符號(hào)蘊(yùn)涵式轉(zhuǎn)化：PQP∨Q；例，Q(x,y)P(y)Q(x,y)∨P(y)。2023/12/25462、合取范式的規(guī)范化過(guò)程③內(nèi)移否認(rèn)符號(hào)使否認(rèn)只出如今原子謂詞公式前，構(gòu)成否認(rèn)文字；狄.摩根定律：(P∨Q)P∧Q(P∧Q)P∨Q雙重否認(rèn)：(P)P量詞否認(rèn)：(x)P(x)(x)(P(x))(x)P(x)(x)(P(x))例，(y)[P(y)∨P(f(x,y))](y)[P(y)∧P(f(x,y))]④變量換名“⑥全稱(chēng)量詞前束化〞后，同名變量的轄域無(wú)法區(qū)分，所以為防止過(guò)失，必需換名；約束變量的虛元性進(jìn)展變換；(x){p(x)=>〔x〕Q〔x〕}

規(guī)范化而得到〔x〕{p(x)=>〔y〕Q〔y〕}2023/12/25472、合取范式的規(guī)范化過(guò)程⑤消去存在量詞〔Skolem變換〕在的轄域內(nèi)(z)(w)[Q(x,z)∨P(z,w)]w依賴(lài)于z，由函數(shù)w=g(z)來(lái)定義這種依賴(lài)關(guān)系；用g(z)來(lái)取代約束變量w，消去存在量詞w；(z)[Q(x,z)∨P(z,g(z))]在多個(gè)的轄域內(nèi)(x)(y)(z)(w)P(x,y,z,w)用多元函數(shù)g(x,y,z)來(lái)取代約束變量w，消去存在量詞w；(x)(y)(z)P(x,y,z,g(x,y,z))在的轄域外(w)(z)[Q(x,z)∨P(z,w)]用恣意常量A取代約束變量w，消去存在量詞w(z)[Q(x,z)∨P(z,A)]前兩種叫Skolem函數(shù)，第三種叫Skolem常量2023/12/2548總結(jié)：Skolem函數(shù)和Skolem常量★

在消去存在量詞的過(guò)程中，需求用到Skolem函數(shù)或Skolem常量。假設(shè)存在量詞是在全稱(chēng)量詞的轄域內(nèi)，用Skolem函數(shù)消去存在量詞。Skolem函數(shù)所運(yùn)用的函數(shù)符號(hào)必需是新的，即不允許是公式中曾經(jīng)出現(xiàn)過(guò)的函數(shù)符號(hào)。假設(shè)要消去的存在量詞不在任何一個(gè)全稱(chēng)量詞的轄域內(nèi)，用不含變量的Skolem函數(shù)即Skolem常量消去存在量詞。所運(yùn)用的常量符號(hào)必需是新的，它未曾在公式其他地方運(yùn)用過(guò)。Skolem變換不是等價(jià)變換，但變換前后的值永假性堅(jiān)持不變。2023/12/25492、合取范式的規(guī)范化過(guò)程⑥全稱(chēng)量詞前束化經(jīng)過(guò)“④變量換名〞后，一切量詞的約束變量均有不同的名字；只需簡(jiǎn)單地將移到適宜公式的最前面；約束變量的作用范圍不會(huì)變化。⑦消去全稱(chēng)量詞經(jīng)過(guò)“⑤消去存在量詞〞后，一切變量均受的約束；簡(jiǎn)單地刪除，只留下母式。⑧把母式轉(zhuǎn)化為合取范式分配律：P∨(Q∧R)(P∨Q)∧(P∨R)2023/12/25502、合取范式的規(guī)范化過(guò)程例、化簡(jiǎn)適宜公式(x){P(x){(y)[P(y)P(f(x,y))]∧(y)(w)[Q(x,y)P(y,w)]}}2023/12/25512、合取范式的規(guī)范化過(guò)程例、化簡(jiǎn)適宜公式(x){P(x){(y)[P(y)P(f(x,y))]∧(y)(w)[Q(x,y)P(y,w)]}}②消去蘊(yùn)涵符號(hào)(x){P(x)∨{(y)[P(y)∨P(f(x,y))]∧(y)(w)[Q(x,y)∨P(y,w)]}}2023/12/25522、合取范式的規(guī)范化過(guò)程例、化簡(jiǎn)適宜公式(x){P(x)∨{(y)[P(y)∨P(f(x,y))]∧(y)(w)[Q(x,y)∨P(y,w)]}} ③內(nèi)移否認(rèn)符號(hào)(x){P(x)∧{(y)[P(y)∧P(f(x,y))]∨(y)(w)[Q(x,y)∨P(y,w)]}}2023/12/25532、合取范式的規(guī)范化過(guò)程例、化簡(jiǎn)適宜公式 (x){P(x)∧{(y)[P(y)∧P(f(x,y))]∨(y)(w)[Q(x,y)∨P(y,w)]}}④變量換名 (x){P(x)∧{(y)[P(y)∧P(f(x,y))]∨(z)(w)[Q(x,z)∨P(z,w)]}}2023/12/25542、合取范式的規(guī)范化過(guò)程例、化簡(jiǎn)適宜公式 (x){P(x)∧{(y)[P(y)∧P(f(x,y))]∨(z)(w)[Q(x,z)∨P(z,w)]}}⑤消去存在量詞{P(A)∧{(y)[P(y)∧P(f(A,y))]∨(z)[Q(A,z)∨P(z,g(z))]}}2023/12/25552、合取范式的規(guī)范化過(guò)程例、化簡(jiǎn)適宜公式{P(A)∧{(y)[P(y)∧P(f(A,y))]∨(z)[Q(A,z)∨P(z,g(z))]}}⑥全稱(chēng)量詞前束化(y)(z){P(A)∧{[P(y)∧P(f(A,y))]∨[Q(A,z)∨P(z,g(z))]}}2023/12/25562、合取范式的規(guī)范化過(guò)程例、化簡(jiǎn)適宜公式(y)(z){P(A)∧{[P(y)∧P(f(A,y))]∨[Q(A,z)∨P(z,g(z))]}}⑦消去全稱(chēng)量詞{P(A)∧{[P(y)∧P(f(A,y))]∨[Q(A,z)∨P(z,g(z))]}}2023/12/25572、合取范式的規(guī)范化過(guò)程例3、化簡(jiǎn)適宜公式{P(A)∧{[P(y)∧P(f(A,y))]∨[Q(A,z)∨P(z,g(z))]}}⑧把母式轉(zhuǎn)化為合取范式{P(A)∧{[P(y)∨Q(A,z)∨P(z,g(z))]∧[P(f(A,y))∨Q(A,z)∨P(z,g(z))]}}完成規(guī)范化過(guò)程！2023/12/2558歸結(jié)演繹推理自動(dòng)定理證明普通表示方式為：F1∧F2∧…∧FnWF1,F2,…,Fn都是適宜公式，表示公理或現(xiàn)實(shí)；W是適宜公式，表示待證明的定理，稱(chēng)為目的公式；證明的方法可分兩大類(lèi)：演繹法直接證明F1∧F2∧…∧FnW為永真；反證法間接證明(F1∧F2∧…∧FnW)為永假；證明F1∧F2∧…∧Fn∧W的永假即{F1,F2,…,Fn}∪{W}是一個(gè)矛盾集。2023/12/2559歸結(jié)演繹推理海伯倫〔Herbrand〕提出的H域〔海伯倫域〕和海伯倫定理；為自動(dòng)定理證明奠定了實(shí)際根底；魯賓遜〔Robinson〕提出的歸結(jié)原理；使自動(dòng)定理證明成為能夠。2023/12/2560歸結(jié)演繹推理

1〕H域和海伯倫定理〔了解〕1、子句和子句集子句——僅由文字的析取∨構(gòu)成的適宜公式Wi=Li1∨Li2∨…∨Lim稱(chēng)為子句；合取范式定義：M=W1∧W2∧…∧WnWi=Li1∨Li2∨…∨Lim(i=1,2,…,n)Lij=Pij|Pij:文字〔Literal〕，是原子謂詞公式Pij或其取反合取范式可定義為子句的合取∧；合取范式表示為子句集，子句間隱含合取∧關(guān)系子句集{W1,W2,…,Wn}2023/12/2561歸結(jié)演繹推理

1〕H域和海伯倫定理1、子句和子句集子句——僅由文字的析取∨構(gòu)成的適宜公式合取范式表示為子句集，子句間隱含具有合取關(guān)系{P(A)∧[P(y)∨Q(A,z)∨P(z,g(z))]∧[P(f(A,y))∨Q(A,z)∨P(z,g(z))]}可進(jìn)一步表示為子句集{P(A),P(y)∨Q(A,z)∨P(z,g(z)),P(f(A,y))∨Q(A,z)∨P(z,g(z))}2023/12/2562歸結(jié)演繹推理

1〕H域和海伯倫定理1、子句和子句集子句——僅由文字的析取∨構(gòu)成的適宜公式合取范式表示為子句集，子句間隱含具有合取關(guān)系(y)(z){P(A)∧[P(y)∨Q(A,z)∨P(z,g(z))]∧[P(f(A,y))∨Q(A,z)∨P(z,g(z))]}量詞分配： (x)[P(x)∧Q(x)](x)P(x)∧(x)Q(x)(y)(z)P(A)∧(y)(z)[P(y)∨Q(A,z)∨P(z,g(z))]∧(y)(z)[P(f(A,y))∨Q(A,z)∨P(z,g(z))]2023/12/2563歸結(jié)演繹推理

1〕H域和海伯倫定理1、子句和子句集子句中的變量都是的約束變量{(y)(z)P(A),(y)(z)[P(y)∨Q(A,z)∨P(z,g(z))],(y)(z)[P(f(A,y))∨Q(A,z)∨P(z,g(z))]}為了消除子句間不用要的交互作用，堅(jiān)持子句的獨(dú)立性，需求做變量換名{P(A),P(y1)∨Q(A,z1)∨P(z1,g(z1)),P(f(A,y2))∨Q(A,z2)∨P(z2,g(z2))}將適宜公式化成字句集，只需求在化成合取范式的根底上，去掉∧符號(hào)以及進(jìn)展變量換名即可。★2023/12/2564總結(jié):子句集的求取1.消去蘊(yùn)涵符號(hào)2.減少否認(rèn)符號(hào)的轄域3.對(duì)變量規(guī)范化4.消去存在量詞5.化為前束形6.把母式化為合取范式7.消去全稱(chēng)量詞8.消去連詞符號(hào)9.改換變量稱(chēng)號(hào)1.消去蘊(yùn)涵符號(hào)只運(yùn)用∨和~符號(hào)，以~A∨B交換A=>B。2.減少否認(rèn)符號(hào)的轄域

每個(gè)否認(rèn)符號(hào)~最多只用到一個(gè)謂詞符號(hào)上，并反復(fù)運(yùn)用狄摩根律。如

以~A∨~B替代~〔A∧B〕

以~A∧~B替代~〔A∨B〕

以A替代~〔~A〕

以(x){~A}替代~〔x〕A

以x){~A}替代~〔x〕A3.對(duì)變量規(guī)范化在任一量詞轄域內(nèi)，受該量詞約束的變量為一啞元〔虛擬變量〕，它可以在該轄域內(nèi)處處一致的被另一個(gè)沒(méi)有出現(xiàn)過(guò)的恣意變量所替代，而不改動(dòng)公式的真值。適宜公式中變量的規(guī)范化意味著對(duì)啞元改名以保證每個(gè)量詞有其本人獨(dú)一的啞元。如，把(x){p(x)=>(x)Q(x)}

規(guī)范化而得到〔x〕{p(x)=>(y)Q(y)}子句：文字的析取組成的公式。如：〔P∨Q∨R〕2023/12/25651.消去蘊(yùn)涵符號(hào)2.減少否認(rèn)符號(hào)的轄域3.對(duì)變量規(guī)范化4.消去存在量詞5.化為前束形6.把母式化為合取范式7.消去全稱(chēng)量詞8.消去連詞符號(hào)9.改換變量稱(chēng)號(hào)4.消去存在量詞在公式〔y〕[〔x〕P〔x，y〕]中，存在量詞是在全稱(chēng)量詞的轄域內(nèi)，我們?cè)试S所存在的x能夠依賴(lài)于y值。令這種依賴(lài)關(guān)系明顯地由函數(shù)g〔y〕所定義，它把每個(gè)y值映射到存在的那個(gè)x。這種函數(shù)就是Skolem函數(shù)。假設(shè)用Skolem函數(shù)替代存在的x，我們就可以消去全部存在量詞〔y〕P[g〔y〕，y]Skolem函數(shù)的變量是由那些全稱(chēng)量詞所約束的全稱(chēng)量詞量化變量，這些全稱(chēng)量詞的轄域包括要被消去的存在量詞的轄域在內(nèi)。Skolem函數(shù)所運(yùn)用的函數(shù)符號(hào)必需是新的。假設(shè)要消去的存在量詞不在任何一個(gè)全稱(chēng)量詞的轄域內(nèi)，那么我們就用不含變量的Skolem函數(shù)即常量。例如，〔x〕P〔x〕化為P〔A〕，其中常量符號(hào)A用來(lái)表示我們知道的存在實(shí)體?？偨Y(jié):子句集的求取2023/12/25661.消去蘊(yùn)涵符號(hào)2.減少否認(rèn)符號(hào)的轄域3.對(duì)變量規(guī)范化4.消去存在量詞5.化為前束形6.把母式化為合取范式7.消去全稱(chēng)量詞8.消去連詞符號(hào)9.改換變量稱(chēng)號(hào)5.化為前束形

如今已不存在任何存在量詞，而且每個(gè)全稱(chēng)量詞都有本人的變量，把一切全稱(chēng)量詞移到公式的左邊，并使每個(gè)量詞的轄域包括這個(gè)量詞后面公式的整個(gè)部分。所得公式稱(chēng)前束形。前束形公式由全稱(chēng)量詞串組成的前綴和不含量詞的母式組成。(x)(y){P(x)∨P(y)}6.把母式化為合取范式

任何母式都可以寫(xiě)成由一些謂詞公式和謂詞公式的否認(rèn)的析取的有限集組成的合取。這種母式叫做合取范式。反復(fù)運(yùn)用分配率，如把A∨{B∧C}化為{A∨B}∧{A∨C}7.消去全稱(chēng)量詞

一切余下的量詞均被全稱(chēng)量詞量化了。全稱(chēng)量詞的次序也不重要了。因此，我們可以消去前綴。8.消去連詞符號(hào)∧

用{A，B}替代{A∧B}，以消去明顯的符號(hào)∧。反復(fù)替代的結(jié)果，最后得到一個(gè)有限集，其中每個(gè)公式是文字的析取。任一只由文字的析取構(gòu)成的適宜公式叫做一個(gè)子句。9.改換變量稱(chēng)號(hào)

改換變量稱(chēng)號(hào)，使一個(gè)變量符號(hào)不出如今一個(gè)以上的子句中。這樣合式公式F化為子句集S后，F(xiàn)和S在永假性上是等價(jià)的總結(jié):子句集的求取2023/12/2567改換變量稱(chēng)號(hào)P(A)

P(y1)∨Q(A,z1)∨P(z1,g(z1))]

P(f(A,y2))∨Q(A,z2)∨P(z2,g(z2))實(shí)例(x){P(x){(y)[P(y)P(f(x,y))]∧(y)(w)[Q(x,y)P(y,w)]}}消去連詞符號(hào)∧P(A)

P(y)∨Q(A,z)∨P(z,g(z))

P(f(A,y))∨Q(A,z)∨P(z,g(z))前面出的計(jì)算的合取范式是{P(A)∧{[P(y)∨Q(A,z)∨P(z,g(z))]∧[P(f(A,y))∨Q(A,z)∨P(z,g(z))]}}2023/12/2568歸結(jié)演繹推理

1〕H域和海伯倫定理1、子句和子句集適宜公式F合取范式子句集S適宜公式F永假子句集S的不可滿(mǎn)足性充分必要條件重要性質(zhì)S的不可滿(mǎn)足性恣意論域D上的恣意解釋I,S中都至少有一個(gè)子句真值為F2023/12/2569歸結(jié)演繹推理

1〕H域和海伯倫定理1、子句和子句集適宜公式F合取范式子句集S適宜公式F永假子句集S的不可滿(mǎn)足性充分必要條件適宜公式F子句集S不等價(jià)S是F的特例重要性質(zhì)S的不可滿(mǎn)足性恣意論域D上的恣意解釋I,S中都至少有一個(gè)子句真值為F2023/12/2570歸結(jié)演繹推理

1〕H域和海伯倫定理2、H域〔了解〕證明子句集S的不可滿(mǎn)足性與證明適宜公式永真性類(lèi)似由于個(gè)體論域的恣意性和解釋個(gè)數(shù)的無(wú)限性，使得證明任務(wù)非常困難。假設(shè)能建造一個(gè)較為簡(jiǎn)單的特殊論域，使得只需證明子句集S在該域不可滿(mǎn)足，就可確保子句集在任何能夠的論域上不可滿(mǎn)足，將是非常有意義的！海伯倫建立的特殊域H就具有這樣的性質(zhì)。H域性質(zhì)——對(duì)于子句集S的任一能夠論域D上的任一解釋I，總能在S的H域上構(gòu)造一個(gè)相應(yīng)的解釋I*，使子句集S具有一樣的真值。證明子句集S的不可滿(mǎn)足性確定子句集S在H域上的一切解釋都不可滿(mǎn)足。2023/12/2571歸結(jié)演繹推理

1〕H域和海伯倫定理3、海伯倫定理〔了解〕子句集S中一子句包含的變量用H域中元素取代后，產(chǎn)生的子句稱(chēng)為基子句。海伯倫定理：子句集S不可滿(mǎn)足的充要條件是存在一個(gè)有限的不可滿(mǎn)足的基子句集S’。有限的不可滿(mǎn)足的基子句集S’子句集S不可滿(mǎn)足性充分必要條件2023/12/2572歸結(jié)演繹推理

2〕歸結(jié)原理★動(dòng)機(jī)為提高斷定子句集S不可滿(mǎn)足的有效性，魯賓遜于1965年提出了歸結(jié)(Resolution)原理，也稱(chēng)為消解原理。歸結(jié)原理簡(jiǎn)單易行，便于計(jì)算機(jī)實(shí)現(xiàn)和執(zhí)行，從而使定理的機(jī)器自動(dòng)證明成為現(xiàn)實(shí)，也成為人工智能技術(shù)適用化的一次重要突破。2023/12/2573歸結(jié)演繹推理

2〕歸結(jié)原理1、歸結(jié)方法(1)歸結(jié)式〔消解式*〕設(shè)有兩個(gè)子句C1=L∨C1’、C2=L∨C2’①?gòu)腃1和C2中消去互補(bǔ)文字L和L；②C1’和C2’經(jīng)過(guò)∨組成新的子句C=C1’∨C2’；稱(chēng)C為C1和C2的歸結(jié)式〔消解式〕；例、兩個(gè)子句C1=P(A)∨Q(x)∨R(f(x))C2=P(A)∨Q(y)∨R(y)消去互補(bǔ)文字P(A)和P(A)后，生成歸結(jié)式：C12=Q(x)∨R(f(x))∨Q(y)∨R(y)C1’C2’2023/12/2574歸結(jié)演繹推理

2〕歸結(jié)原理1、歸結(jié)方法(2)歸結(jié)式性質(zhì)定理：兩個(gè)子句C1和C2的歸結(jié)式C是C1和C2的邏輯推論任一使子句C1和C2為真的解釋I，必使歸結(jié)式C為真；歸結(jié)式C為假的解釋I，子句C1或者C2為假；推論：設(shè)C1和C2是子句集S中的兩個(gè)子句，并以C作為它們的歸結(jié)式；經(jīng)過(guò)往S中參與C而產(chǎn)生的擴(kuò)展子句集S’與子句集S在不可滿(mǎn)足的意義上是等價(jià)的！歸結(jié)后擴(kuò)展子句集S’子句集S不可滿(mǎn)足性等價(jià)2023/12/2575歸結(jié)演繹推理

2〕歸結(jié)原理1、歸結(jié)方法(3)空子句設(shè)C1=L、C2=L，那么歸結(jié)式C為空；以□表示為空的歸結(jié)式C，并稱(chēng)C=□為空子句；由于C1和C2是一對(duì)矛盾子句，不可同時(shí)滿(mǎn)足，所以□是不可滿(mǎn)足的子句；經(jīng)過(guò)往S中參與□而產(chǎn)生的擴(kuò)展子句集S’不可滿(mǎn)足；空子句□是用歸結(jié)原理斷定子句集S不可滿(mǎn)足的勝利標(biāo)志。歸結(jié)后的擴(kuò)展子句集S’子句集S不可滿(mǎn)足性等價(jià)2023/12/2576(1)假言推理父輩子句P~P∨Q〔即P=>Q〕消解式QC1=P,C2=~P∨Q〔2〕合并C1=P∨Q,C2=~P∨Q父輩子句P∨Q~P∨Q消解式Q∨Q＝Q對(duì)基子句的消解2023/12/2577(3)重言式父輩子句P∨Q~P∨~Q消解式Q∨~QC1=P∨Q,C2=~P∨~Q父輩子句P∨Q~P∨~Q消解式P∨~P或者2023/12/2578(4)空子句(矛盾)P~PNIL〔5〕鏈?zhǔn)健踩握摗硚P∨R,(即P=>R)~R∨Q,(即R=>Q)~P∨Q,(即P=>Q)2023/12/2579歸結(jié)演繹推理

2〕歸結(jié)原理動(dòng)機(jī)為提高斷定子句集S不可滿(mǎn)足的有效性，魯賓遜于1965年提出了歸結(jié)(Resolution)原理，也稱(chēng)為消解原理。歸結(jié)原理簡(jiǎn)單易行，便于計(jì)算機(jī)實(shí)現(xiàn)和執(zhí)行，從而使定理的機(jī)器自動(dòng)證明成為現(xiàn)實(shí)，也成為人工智能技術(shù)適用化的一次重要突破。根本思緒★經(jīng)過(guò)歸結(jié)方法不斷擴(kuò)展待斷定的子句集S，并設(shè)法使其包含進(jìn)指示矛盾的空子句?？兆泳涫遣豢蓾M(mǎn)足〔即永假〕的子句；2023/12/2580歸結(jié)演繹推理

2〕歸結(jié)原理2、歸結(jié)推理過(guò)程——?dú)w結(jié)演繹樹(shù)(1)命題邏輯中的歸結(jié)推理過(guò)程子句中文字只是原子命題公式或其取反，不帶變量；易于判別哪些子句對(duì)包含互補(bǔ)文字；例、子句集S={P∨Q,P∨R,Q,R}的歸結(jié)演繹樹(shù)。2023/12/2581歸結(jié)演繹推理

2〕歸結(jié)原理2、歸結(jié)推理過(guò)程(1)命題邏輯中的歸結(jié)推理過(guò)程例、子句集S={P∨Q,P∨R,Q,R}的歸結(jié)演繹樹(shù)。擴(kuò)展子句集S’包含空子句子句集S不可滿(mǎn)足2023/12/2582歸結(jié)演繹推理

2〕歸結(jié)原理-置換和合一★2、歸結(jié)推理過(guò)程(2)謂詞邏輯中的歸結(jié)推理過(guò)程子句中含有變量，不能直接發(fā)現(xiàn)和消去互補(bǔ)文字；需對(duì)潛在的互補(bǔ)文字先作變量置換和合一處置。變量置換：用置換項(xiàng)取代公式中的變量；置換項(xiàng)可以是變量、常量或函數(shù)。置換元素——t/v〔置換項(xiàng)/變量〕置換——假設(shè)干置換元素的集合；合一處置：P(x,y,x,g(x)),P(A,B,A,z)2023/12/2583

P(x,y,x,g(x)),P(A,B,A,z)我們可以為它們建立多個(gè)置換：

S1={A/x,B/y,g(x)/z}

S2={f(w)/x,z/y,C/z}

S3={B/x,f(w)/y,y/z}

置換結(jié)果為：

{P(x,y,x,g(x)),P(A,B,A,z)}S1

={P(A,B,A,g(A)),P(A,B,A,g(A))}

{P(x,y,x,g(x)),P(A,B,A,z)}S2

={P(f(w)),z,f(w),g(f(w)),P(A,B,A,C)}

{P(x,y,x,g(x)),P(A,B,A,z)}S3

={P(B,f(w),B,g(B)),P(A,B,A,y)}

S1使?jié)撛诘幕パa(bǔ)文字中的原子謂詞公式變?yōu)橥?，確認(rèn)互補(bǔ)性。2023/12/2584置換和合一實(shí)例1將它們分別作用于表達(dá)式，得：P[x，f〔y〕，B]s1=P[z，f〔w〕，B]P[x，f〔y〕，B]s2=P[x，f〔A〕，B]P[x，f〔y〕，B]s3=P[q〔z〕，f〔A〕，B]P[x，f〔y〕，B]s4=P[c，f〔A〕，B]表達(dá)式P[x，f〔y〕，B]的4個(gè)置換為

s1={z/x，w/y}

s2={A/y}

s3={q〔z〕/x，A/y}

s4={c/x，A/y}2023/12/2585置換和合一實(shí)例2置換是可結(jié)合的。用s1s2表示兩個(gè)置換s1和s2的合成。L表示一表達(dá)式，那么有

〔Ls1〕s2=L〔s1s2〕

〔s1s2〕s3=s1〔s2s3〕

置換是不可交換的。即

s1s2s2s12023/12/2586歸結(jié)演繹推理

2〕歸結(jié)原理-置換和合一2、歸結(jié)推理過(guò)程(2)謂詞邏輯中的歸結(jié)推理過(guò)程子句中含有變量，不能直接發(fā)現(xiàn)和消去互補(bǔ)文字；需對(duì)潛在的互補(bǔ)文字先作變量置換和合一處置。變量置換：用置換項(xiàng)取代公式中的變量；置換項(xiàng)可以是變量、常量或函數(shù)。置換元素——t/v〔置換項(xiàng)/變量〕置換——假設(shè)干置換元素的集合；合一處置：經(jīng)過(guò)多個(gè)變量置換，使相應(yīng)于潛在互補(bǔ)文字的原子謂詞公式同一化的過(guò)程。P(x,y,x,g(x)),P(A,B,A,z)2023/12/2587歸結(jié)演繹推理

2〕歸結(jié)原理-置換和合一2、歸結(jié)推理過(guò)程(2)謂詞邏輯中的歸結(jié)推理過(guò)程經(jīng)過(guò)一個(gè)匹配過(guò)程去檢查兩個(gè)原子謂詞公式的可合一性，并同時(shí)建立用于實(shí)現(xiàn)合一的置換?！酒ヅ溥^(guò)程】★①兩個(gè)原子謂詞公式必需具有一樣的謂詞符號(hào)和參數(shù)項(xiàng)個(gè)數(shù)；②從左到右逐個(gè)檢查每對(duì)參數(shù)項(xiàng)的可合一性；③假設(shè)每對(duì)參數(shù)項(xiàng)都可合一，那么合一處置勝利，并建立用于實(shí)現(xiàn)合一的置換。2023/12/2588歸結(jié)演繹推理

2〕歸結(jié)原理-置換和合一【匹配過(guò)程】②從左到右逐個(gè)檢查每對(duì)參數(shù)項(xiàng)的可合一性；參數(shù)對(duì)中有一個(gè)是變量v〔不關(guān)懷另一個(gè)t能否是變量〕v初次出現(xiàn)，參數(shù)對(duì)可合一，以另一參數(shù)t為置換項(xiàng)，構(gòu)成置換元素t/v;v出現(xiàn)過(guò)，那么已建立相應(yīng)的置換元素，就取其置換項(xiàng)，替代該變量，檢查能否與另一參數(shù)同一；假設(shè)不同一，那么處置失??；參數(shù)對(duì)中沒(méi)有變量，那么必需一樣，否那么合一處置失敗。2023/12/2589歸結(jié)演繹推理

2〕歸結(jié)原理-置換和合一2、歸結(jié)推理過(guò)程(2)謂詞邏輯中的歸結(jié)推理過(guò)程匹配過(guò)程的例子P(x,y,x,g(x)),P(A,B,A,z)①兩個(gè)原子謂詞公式必需具有一樣的謂詞和參數(shù)項(xiàng)個(gè)數(shù)；②從左到右逐個(gè)檢查每對(duì)參數(shù)項(xiàng)的可合一性；x和A，x初次出現(xiàn)，可合一，建立置換元素A/x;y和B，y初次出現(xiàn)，可合一，建立置換元素B/y;x和A，x出現(xiàn)過(guò)，曾經(jīng)建立置換元素A/x，可合一；g(x)和z，z初次出現(xiàn)，可合一，建立置換元素g(x)/z；③假設(shè)每對(duì)參數(shù)項(xiàng)都可合一，那么合一處置勝利。建立置換S1={A/x,B/y,g(x)/z}2023/12/2590歸結(jié)演繹推理

2〕歸結(jié)原理-置換和合一2、歸結(jié)推理過(guò)程(2)謂詞邏輯中的歸結(jié)推理過(guò)程謂詞邏輯中子句歸結(jié)的例子：C1=P(x,y)∨Q(x,f(x))∨R(x,f(y))C2=P(A,B)∨Q(z,f(z))∨R(z,f(z))L11=P(x,y)和L12=P(A,B)是潛在的互補(bǔ)文字L11和L12是可合一的；建立置換S1={A/x,B/y}消去互補(bǔ)文字L11和L12后，得歸結(jié)式：Q(A,f(A))∨R(A,f(B))∨Q(z,f(z))∨R(z,f(z))變量的置換必需在整個(gè)子句范圍內(nèi)進(jìn)展2023/12/2591歸結(jié)演繹推理

2〕歸結(jié)原理-置換和合一2、歸結(jié)推理過(guò)程(2)謂詞邏輯中的歸結(jié)推理過(guò)程謂詞邏輯中子句歸結(jié)的例子：C1=P(x,y)∨Q(x,f(x))∨R(x,f(y))C2=P(A,B)∨Q(z,f(z))∨R(z,f(z))L21=Q(x,f(x))和L22=Q(z,f(z))是潛在的互補(bǔ)文字L21和L22是可合一的；建立置換S2={z/x}消去互補(bǔ)文字L21和L22后，得歸結(jié)式：P(z,y)∨R(z,f(y))∨P(A,B)∨R(z,f(z))2023/12/2592歸結(jié)演繹推理

2〕歸結(jié)原理-置換和合一2、歸結(jié)推理過(guò)程(2)謂詞邏輯中的歸結(jié)推理過(guò)程謂詞邏輯中子句歸結(jié)的例子：C1=P(x,y)∨Q(x,f(x))∨R(x,f(y))C2=P(A,B)∨Q(z,f(z))∨R(z,f(z))L11=P(x,y)和L12=P(A,B)是互補(bǔ)文字L21=Q(x,f(x))和L22=Q(z,f(z))是互補(bǔ)文字兩個(gè)子句可以有多于一對(duì)的互補(bǔ)文字2023/12/2593置換和合一實(shí)例3求公式集

F={P(a，x，f(g(y)))，P(z，h(z，u)，f(u))}的合一。第一對(duì)參數(shù)是可同一的，用z/a,第二對(duì)參數(shù)也是可同一的，由于z曾經(jīng)出現(xiàn)過(guò)，所以用a換z,然后用h(a,u)/x第三對(duì)參數(shù)可用g(y)/u所以該公式是可同一的，可建立置換S1={z/a,h(a,u)/x,g(y)/u}2023/12/2594歸結(jié)演繹推理

2〕歸結(jié)原理2、歸結(jié)推理過(guò)程(2)謂詞邏輯中的歸結(jié)推理過(guò)程2023/12/2595歸結(jié)演繹推理

2〕歸結(jié)原理2、歸結(jié)推理過(guò)程(2)謂詞邏輯中的歸結(jié)推理過(guò)程2023/12/2596歸結(jié)演繹推理

2〕歸結(jié)原理2、歸結(jié)推理過(guò)程(2)謂詞邏輯中的歸結(jié)推理過(guò)程2023/12/2597歸結(jié)演繹推理

2〕歸結(jié)原理2、歸結(jié)推理過(guò)程(2)謂詞邏輯中的歸結(jié)推理過(guò)程子句集S不可滿(mǎn)足2023/12/2598歸結(jié)演繹推理

2〕歸結(jié)原理2、歸結(jié)推理過(guò)程(3)歸結(jié)演繹的完備性基于歸結(jié)的演繹推理是完備的假設(shè)子句集S不可滿(mǎn)足，就必定存在一個(gè)從S到空子句□的歸結(jié)演繹；反之，假設(shè)存在一個(gè)從S到空子句□的歸結(jié)演繹，那么S必定是不可滿(mǎn)足的；歸結(jié)演繹的完備性可用海伯倫定理進(jìn)展證明，因此歸結(jié)原理是建立在海伯倫定理之上的。但歸結(jié)原理并不能用于處理子句集不可滿(mǎn)足性的不可判問(wèn)題，即假設(shè)子句集S是永真的和可滿(mǎn)足的，歸結(jié)原理斷定過(guò)程將無(wú)休止地進(jìn)展下去，得不到任何結(jié)果。2023/12/2599歸結(jié)演繹推理

3〕歸結(jié)反演★歸結(jié)演繹推理為反證法證明定理提供了有效手段。運(yùn)用歸結(jié)演繹推理的定理證明為歸結(jié)反演。教學(xué)要求——掌握主要內(nèi)容掌握歸結(jié)反演方法和提取問(wèn)題回答技術(shù)；學(xué)會(huì)建立歸結(jié)反演樹(shù)和修正證明樹(shù)。學(xué)習(xí)難點(diǎn)從以自然言語(yǔ)表示的現(xiàn)實(shí)集證明目的公式〔定理〕并提取回答的綜合題。2023/12/25100歸結(jié)反演的原理欲證F1∧F2∧…∧FnW永真，可以經(jīng)過(guò)F1∧F2∧…∧Fn∧W的永假來(lái)證明。適宜公式F永假子句集S的不可滿(mǎn)足性充分必要條件有限的不可滿(mǎn)足的基子句集S’子句集S不可滿(mǎn)足性充分必要條件歸結(jié)后擴(kuò)展子句集S’子句集S不可滿(mǎn)足性等價(jià)歸結(jié)的演繹推理的完備性：假設(shè)子句集S不可滿(mǎn)足，就必定存在一個(gè)從S到空子句□的歸結(jié)演繹；反之亦然。2023/12/25101歸結(jié)演繹推理

3〕歸結(jié)反演——?dú)w結(jié)反演系統(tǒng)歸結(jié)反演的根本思緒：要從作為現(xiàn)實(shí)的公式集F證明目的公式W為真；①先將W取反W，參與公式集F；②規(guī)范化F∧W為子句集S；③經(jīng)過(guò)歸結(jié)演繹證明S不可滿(mǎn)足，得出W為真的結(jié)論。歸結(jié)反演系統(tǒng)組成：規(guī)范化部件將F∧W規(guī)范化為子句，并合并為子句集S；歸結(jié)演繹部件按照歸結(jié)演繹推理，控制定理證明的全過(guò)程。2023/12/25102歸結(jié)演繹推理

3〕歸結(jié)反演——?dú)w結(jié)反演系統(tǒng)例、歸結(jié)反演的運(yùn)用——食物問(wèn)題知以下現(xiàn)實(shí)為真T，王(Wang)喜歡(Like)一切種類(lèi)的食物(Food)。蘋(píng)果(Apples)是食物。任何一個(gè)東西，假設(shè)任何人吃了(Eat)它都不會(huì)被害死(Killed)，那么該東西是食物。李(Li)吃花生(Peanuts)且依然活著(Alive)。張(Zhang)吃任何李吃的東西。證明：王喜歡花生。2023/12/25103歸結(jié)演繹推理

3〕歸結(jié)反演——?dú)w結(jié)反演系統(tǒng)例、歸結(jié)反演的運(yùn)用——食物問(wèn)題①方式化——把以自然言語(yǔ)表示的現(xiàn)實(shí)和要證明的目的方式化地表示為適宜公式。王(Wang)喜歡(Like)一切種類(lèi)的食物(Food)。(x)[Food(x)Like(Wang,x)]蘋(píng)果(Apples)是食物。Food(Apples)任何一個(gè)東西，假設(shè)任何人吃了(Eat)它都不會(huì)被害死(Killed)，那么該東西是食物。(x)(y)[Eat(y,x)∧Killed(y)Food(x)](x)(y)[Eat(y,x)∧Alive(y)Food(x)]李(Li)吃花生(Peanuts)且依然活著(Alive)。Eat(Li,Peanuts)∧Alive(Li)張(Zhang)吃任何李吃的東西。(x)[Eat(Li,x)Eat(Zhang,x)]王喜歡花生。Like(Wang,Peanuts)減少謂詞數(shù)2023/12/25104歸結(jié)演繹推理

3〕歸結(jié)反演——?dú)w結(jié)反演系統(tǒng)例、歸結(jié)反演的運(yùn)用——食物問(wèn)題②規(guī)范化——將現(xiàn)實(shí)公式和取反后的目的公式分別規(guī)范化為子句，并組成子句集S。王(Wang)喜歡(Like)一切種類(lèi)的食物(Food)。(x)[Food(x)Like(Wang,x)]Food(x1)∨Like(Wang,x1)蘋(píng)果(Apples)是食物。Food(Apples)Food(Apples)任何一個(gè)東西，假設(shè)任何人吃了(Eat)它都不會(huì)被害死(Killed)，那么該東西是食物。(x)(y)[Eat(y,x)∧Alive(y)Food(x)]Eat(y,x2)∨Alive(y)∨Food(x2)2023/12/25105歸結(jié)演繹推理

3〕歸結(jié)反演——?dú)w結(jié)反演系統(tǒng)例、歸結(jié)反演的運(yùn)用——食物問(wèn)題②規(guī)范化——將現(xiàn)實(shí)公式和取反后的目的公式分別規(guī)范化為子句，并組成字句集S。李(Li)吃花生(Peanuts)且依然活著(Alive)。Eat(Li,Peanuts)∧Alive(Li)Eat(Li,Peanuts)Alive(Li)張(Zhang)吃任何李吃的東西。(x)[Eat(Li,x)Eat(Zhang,x)]Eat(Li,x3)∨Eat(Zhang,x3)王喜歡花生。Like(Wang,Peanuts)Like(Wang,Peanuts)取反2023/12/25106歸結(jié)演繹推理

3〕歸結(jié)反演——?dú)w結(jié)反演系統(tǒng)例、歸結(jié)反演的運(yùn)用——食物問(wèn)題③歸結(jié)演繹——運(yùn)用歸結(jié)演繹推理不斷生成歸結(jié)式以擴(kuò)展子句集S，直到生成空子句□。2023/12/25107歸結(jié)演繹推理

3〕歸結(jié)反演——?dú)w結(jié)反演系統(tǒng)例、歸結(jié)反演的運(yùn)用——食物問(wèn)題③歸結(jié)演繹——運(yùn)用歸結(jié)演繹方法不斷生成歸結(jié)式以擴(kuò)展子句集S，直到生成空子句□。2023/12/25108歸結(jié)演繹推理

3〕歸結(jié)反演——?dú)w結(jié)反演系統(tǒng)例、歸結(jié)反演的運(yùn)用——食物問(wèn)題③歸結(jié)演繹——運(yùn)用歸結(jié)演繹方法不斷生成歸結(jié)式以擴(kuò)展子句集S，直到生成空子句□。2023/12/25109歸結(jié)演繹推理

3〕歸結(jié)反演——?dú)w結(jié)反演系統(tǒng)例、歸結(jié)反演的運(yùn)用——食物問(wèn)題③歸結(jié)演繹——運(yùn)用歸結(jié)演繹方法不斷生成歸結(jié)式以擴(kuò)展子句集S，直到生成空子句□。2023/12/25110歸結(jié)演繹推理

3〕歸結(jié)反演——?dú)w結(jié)反演系統(tǒng)例、歸結(jié)反演的運(yùn)用——食物問(wèn)題③歸結(jié)演繹——運(yùn)用歸結(jié)演繹方法不斷生成歸結(jié)式以擴(kuò)展子句集S，直到生成空子句□。目的公式得證歸結(jié)反演樹(shù)2023/12/25111例

前提：每個(gè)儲(chǔ)蓄錢(qián)的人都獲得利息。

結(jié)論：假設(shè)沒(méi)有利息，那么就沒(méi)有人去儲(chǔ)蓄錢(qián)。令：S〔x，y〕表示x儲(chǔ)蓄y

M〔x〕表示x是錢(qián)

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)(M(y)=>~S(x，y))歸結(jié)演繹推理

3〕歸結(jié)反演——?dú)w結(jié)反演系統(tǒng)2023/12/25112把前提化為子句形：

(x)(~(y)(S(x，y)∧M(y))∨(y)(I(y)∧E(x，y)))

(x)((y)(~(S(x，y)∧M(y)))∨〔y〕〔I〔y〕∧E〔x，y〕〕〕

(x)((y)(~S(x，y)∨~M〔y〕〕∨〔y〕〔I〔y〕∧E〔x，y〕〕〕令y=f(x)為Skolem函數(shù)，那么得子句形

(x)(y)((~S(x，y)∨~M(y)∨I(f(x)))∧(~S(x，y)∨M(y)∨E(x，f〔x〕〕〕

〔1〕~S〔x，y〕∨~M〔y〕∨I〔f〔x〕〕

〔2〕~S〔x，y〕∨~M〔y〕∨E〔x，f〔x〕〕〕歸結(jié)演繹推理

3〕歸結(jié)反演——?dú)w結(jié)反演系統(tǒng)2023/12/25113結(jié)論的否以為

~〔~〔x〕I〔x〕=>〔x〕〔y〕〔M〔y〕=>~S〔x，y〕〕〕

化為子句形

~〔〔x〕I〔x〕∨〔x〕〔y〕〔~M〔y〕∨~S〔x，y〕〕〕

〔~〔x〕I〔x〕∧〔~〔x〕〔y〕〔~M〔y〕∨~S〔x，y〕〕〕〕

〔x〕〔~I〔x〕〕∧〔x〕〔y〕〔M〔y〕∧S〔x，y〕〕變量分別規(guī)范化后得以下子句：

〔3〕~I〔z〕

〔4〕S〔a，b〕

〔5〕

M〔b〕歸結(jié)演繹推理

3〕歸結(jié)反演——?dú)w結(jié)反演系統(tǒng)2023/12/25114儲(chǔ)蓄問(wèn)題的反演樹(shù)歸結(jié)演繹推理

3〕歸結(jié)反演——?dú)w結(jié)反演系統(tǒng)〔1〕~S〔x，y〕∨~M〔y〕∨I〔f〔x〕〕

〔2〕~S〔x，y〕∨~M〔y〕∨E〔x，f〔x〕〕〕〔3〕~I〔z〕

〔4〕S〔a，b〕

〔5〕

M〔b〕2023/12/25115歸結(jié)演繹推理

3〕歸結(jié)反演:課堂練習(xí)某公司招聘任務(wù)人員，A，B，C三人應(yīng)試，經(jīng)面試后，公司表示如下想法：〔1〕三人中至少錄取一人?！?〕假設(shè)錄取A而不錄取B，那么一定錄取C?！?〕假設(shè)錄取B，那么一定錄取C。用歸結(jié)反演法證明：公司一定錄取C?！蔡崾荆涸O(shè)用P(x)表示錄取x〕2023/12/25116歸結(jié)演繹推理

3〕歸結(jié)反演把公司的想法用謂詞公式表示如下：〔1〕三人中至少錄取一人。P(A)∨P(B)∨P(C)〔2〕假設(shè)錄取A而不錄取B，那么一定錄取C。P(A)∧P(B)P(C)〔3〕假設(shè)錄取B，那么一定錄取C。P(B)P(C)把要求證的問(wèn)題否認(rèn)，并用謂詞公式表示出來(lái)：公司一定錄取CP(C)2023/12/25117歸結(jié)演繹推理

3〕歸結(jié)反演把上述公式化成子句集①P(A)∨P(B)∨P(C)②P(A)∨P(B)∨P(C)③P(B)∨P(C)④P(C)運(yùn)用歸結(jié)反演：①②P(B)∨P(C)③P(C)④2023/12/25118歸結(jié)演繹推理

3〕歸結(jié)反演——提取問(wèn)題回答某記者到一個(gè)孤島采訪(fǎng)，遇到一個(gè)難題，即島上有許多人說(shuō)假話(huà)，因此難以保證新聞報(bào)道的正確性，不過(guò)有一點(diǎn)他是清楚的，這個(gè)島上的人有一個(gè)特點(diǎn)：說(shuō)假話(huà)的人從來(lái)不說(shuō)真話(huà)，說(shuō)真話(huà)的人從來(lái)不說(shuō)假話(huà)；一次，記者遇到了孤島上的3個(gè)人，為了弄清誰(shuí)說(shuō)真話(huà)，誰(shuí)說(shuō)假話(huà)，他向這3個(gè)人中的每一個(gè)都提了一個(gè)同樣的問(wèn)題“誰(shuí)是說(shuō)謊者？〞A回答：B和C都是說(shuō)謊者。B回答：A和C都是說(shuō)謊者。C回答：A和B中至少有一個(gè)是說(shuō)謊者。誰(shuí)是說(shuō)謊者？2023/12/25119歸結(jié)演繹推理

3〕歸結(jié)反演——提取問(wèn)題回答設(shè)A、B、C三個(gè)命題表示A、B、C三人是老實(shí)人。A回答：B和C都是說(shuō)謊者。AB∧CAB∨CB回答：A和C都是說(shuō)謊者。BA∧CBA∨CC回答：A和B中至少有一個(gè)是說(shuō)謊者。CA∨BCA∧B2023/12/25120歸結(jié)演繹推理

3〕歸結(jié)反演——提取問(wèn)題回答設(shè)A、B、C三個(gè)命題表示A、B、C三人是老實(shí)人?；?jiǎn)上述蘊(yùn)含式為子句集①A∨B②A(yíng)∨C③A∨B∨C④B∨C⑤A∨B∨C⑥A∨C⑦B∨C①和⑦歸結(jié)：A∨C⑧②和⑧歸結(jié)：A⑨⑥和⑨歸結(jié)：C⑩④和⑩歸結(jié)：B結(jié)論：A和B都是說(shuō)謊者，而C是老實(shí)人2023/12/25121例:王某被害，有四個(gè)嫌疑犯A，B，C，D，公安局派出五個(gè)偵查員，他們帶回的信息各不一樣，甲說(shuō)A，B中至少有一人作案，乙說(shuō)B，C中至少有一人作案，丙說(shuō)C，D中至少有一人作案，丁說(shuō)A，C中至少有一人與此案無(wú)關(guān)，戊說(shuō)B，D中至少有一人與此案無(wú)關(guān)，假設(shè)這五個(gè)偵查員的話(huà)都是可靠的，那么誰(shuí)是罪犯。2023/12/25122〔1〕A∨B〔2〕B∨C〔3〕C∨D〔4〕~A∨~C〔5〕~B∨~D〔6〕B∨~C〔1〕、〔4〕歸結(jié)；〔7〕B是罪犯。〔2〕、〔6〕歸結(jié)；〔8〕C∨~D〔2〕、〔5〕歸結(jié)；〔9〕C是罪犯?！?〕、〔8〕歸結(jié)。2023/12/25123歸結(jié)反演可實(shí)現(xiàn)問(wèn)題回答系統(tǒng)目的公式往往受存在量詞約束，如(x)W(x)；不僅證明目的公式為真T；回答提取——給出使W(x)為真T的x的某個(gè)取值。問(wèn)題回答系統(tǒng)分為2個(gè)階段：①歸結(jié)反演——證明目的公式為真T②回答提取對(duì)于規(guī)范化取反的目的公式而產(chǎn)生的子句〔稱(chēng)為目的子句〕G,建立其重言式〔永真式〕G∨G；以G∨G取代G,反復(fù)已進(jìn)展過(guò)的歸結(jié)演繹過(guò)程，建立修正證明樹(shù)。結(jié)果——修正證明樹(shù)的樹(shù)根不再是空子句□，而是G，且G中的變量已為其置換項(xiàng)取代，實(shí)現(xiàn)了回答提取。歸結(jié)演繹推理

3〕歸結(jié)反演——提取問(wèn)題回答2023/12/25124歸結(jié)演繹推理

3〕歸結(jié)反演——提取問(wèn)題回答例、提取問(wèn)題回答的運(yùn)用——食物問(wèn)題知以下現(xiàn)實(shí)為真，王(Wang)喜歡(Like)一切種類(lèi)的食物(Food)。蘋(píng)果(Apples)是食物。任何一個(gè)東西，假設(shè)任何人吃了(Eat)它都不會(huì)被害死(Killed)，那么該東西是食物。李(Li)吃花生(Peanuts)且依然活著(Alive)。張(Zhang)吃任何李吃的東西。證明：王喜歡花生。問(wèn)題：張吃什么食物？2023/12/25125歸結(jié)演繹推理

3〕歸結(jié)反演——提取問(wèn)題回答例、提取問(wèn)題回答的運(yùn)用——食物問(wèn)題(1)方式化王(Wang)喜歡(Like)一切種類(lèi)的食物(Food)。(x)[Food(x)Like(Wang,x)]蘋(píng)果(Apples)是食物。Food(Apples)任何一個(gè)東西，假設(shè)任何人吃了(Eat)它都不會(huì)被害死(Killed)，那么該東西是食物。(x)(y)[Eat(y,x)∧Alive(y)Food(x)]李(Li)吃花生(Peanuts)且依然活著(Alive)。Eat(Li,Peanuts)∧Alive(Li)張(Zhang)吃任何李吃的東西。(x)[Eat(Li,x)Eat(Zhang,x)]問(wèn)題“張吃什么食物？〞方式化為目的公式(x)[Food(x)∧Eat(Zhang,x)]2023/12/25126歸結(jié)演繹推理

3〕歸結(jié)反演——提取問(wèn)題回答例、提取問(wèn)題回答的運(yùn)用——食物問(wèn)題(2)規(guī)范化目的子句G目的公式取反各個(gè)子句變量不要重名2023/12/25127歸結(jié)演繹推理

3〕歸結(jié)反演——提取問(wèn)題回答例、提取問(wèn)題回答的運(yùn)用——食物問(wèn)題①歸結(jié)反演歸結(jié)反演樹(shù)(x)[Food(x)∧Eat(Zhang,x)]2023/12/25128歸結(jié)演繹推理

3〕歸結(jié)反演——提取問(wèn)題回答例、提取問(wèn)題回答的運(yùn)用——食物問(wèn)題②回答提取——(1)建立重言式G∨G目的子句G目的公式G目的子句G建立重言式G∨G取反2023/12/25129歸結(jié)演繹推理

3〕歸結(jié)反演——提取問(wèn)題回答例、提取問(wèn)題回答的運(yùn)用——食物問(wèn)題②回答提取——(2)以G∨G取代G,反復(fù)已進(jìn)展過(guò)的歸結(jié)演繹過(guò)程，建立修正證明樹(shù)。建立修正證明樹(shù)過(guò)程中：1、重言式G∨G中的G并不真正參與歸結(jié)演繹；2、G∨G取代G反復(fù)歸結(jié)演繹過(guò)程，只是為了使G中的變量隨著G中出現(xiàn)的變量置換而同時(shí)得到置換。2023/12/25130修正證明樹(shù)2023/12/25131歸結(jié)演繹推理

3〕歸結(jié)反演——提取問(wèn)題回答例、提取問(wèn)題回答的運(yùn)用——食物問(wèn)題②回答提取——(2)以G∨G取代G,反復(fù)已進(jìn)展過(guò)的歸結(jié)演繹過(guò)程，建立修正證明樹(shù)。建立修正證明樹(shù)過(guò)程中：1、重言式G∨G中的G并不真正參與歸結(jié)演繹；2、G∨G取代G反復(fù)歸結(jié)演繹過(guò)程，只是為了使G中的變量隨著G中出現(xiàn)的變量置換而同時(shí)得到置換。3、①歸結(jié)反演和②回答提取可以合為一體進(jìn)展，一次性生成修正證明樹(shù)。防止誤用G參與歸結(jié)，可以用特定的符號(hào)替代G。例如、ANSWER(x1,x2,…,xn)，xi是G中的變量。2023/12/25132修正證明樹(shù)2023/12/25133歸結(jié)演繹推理

3〕歸結(jié)反演——提取問(wèn)題回答從適用的角度，目的公式或許會(huì)取更為復(fù)雜的方式①目的公式取反后的化簡(jiǎn)結(jié)果是多個(gè)子句的合取(x)(y){[A(x)∧B(x)]∨[C(y)∧D(y)]}取反化簡(jiǎn)后[A(x)∨B(x)]∧[C(y)∨D(y)]建立2個(gè)重言式A(x)∨B(x)∨[A(x)∧B(x)]C(y)∨D(y)∨[C(y)∧D(y)]②目的公式含有全稱(chēng)量詞(x)(y)(z)(w)P(x,y,z,w)取反后(x)(y)(z)(w)P(x,y,z,w)消去量詞P(A,y,z,g(y,z))如何處置函數(shù)g(y,z)超出范圍，不做引見(jiàn)。2023/12/25134歸結(jié)演繹推理

3〕歸結(jié)反演——?dú)w結(jié)戰(zhàn)略歸結(jié)反演面臨大子句集S引起演繹效率問(wèn)題處理的關(guān)鍵是選擇有利于導(dǎo)致快速產(chǎn)生空子句□的子句對(duì)進(jìn)展歸結(jié)支持集；線(xiàn)性輸入；單文字子句優(yōu)先；祖先過(guò)濾；歸結(jié)反演技術(shù)并未在定理自動(dòng)證明以外的領(lǐng)域得到廣泛運(yùn)用。2023/12/25135歸結(jié)演繹推理的歸結(jié)戰(zhàn)略

-廣度優(yōu)先戰(zhàn)略廣度優(yōu)先是一種窮盡子句比較的復(fù)雜搜索方法。設(shè)初始子句集為S0，廣度優(yōu)先戰(zhàn)略的歸結(jié)過(guò)程可描畫(huà)如下：(1)從S0出發(fā)，對(duì)S0中的全部子句作一切能夠的歸結(jié)，得到第一層歸結(jié)式，把這些歸結(jié)式的集合記為S1;(2)用S0中的子句與S1中的子句進(jìn)展一切能夠的歸結(jié)，得到第二層歸結(jié)式，把這些歸結(jié)式的集合記為S2;(3)用S0和S1中的子句與S2中的子句進(jìn)展一切能夠的歸結(jié)，得到第三層歸結(jié)式，把這些歸結(jié)式的集合記為S3;如此繼續(xù)，知道得出空子句或不能再繼續(xù)歸結(jié)為止。2023/12/25136﹁I(x)∨R(x)I(a)﹁R(y)∨L(y)﹁L(a)R(a)﹁I(x)∨L(x)﹁R(a)L(a)L(a)﹁I(a)﹁I(a)NILSS1S2例設(shè)有如下子句集：S={﹁I(x)∨R(x),I(a),﹁R(y)∨L(y),﹁L(a)}用寬度優(yōu)先戰(zhàn)略證明S為不可滿(mǎn)足。寬度優(yōu)先戰(zhàn)略的歸結(jié)樹(shù)如下：2023/12/25137寬度優(yōu)先戰(zhàn)略歸結(jié)出了許多無(wú)用的子句，既浪費(fèi)時(shí)間，又浪費(fèi)空間。但是，這種戰(zhàn)略有一個(gè)有趣的特性，就是當(dāng)問(wèn)題有解時(shí)保證能找到最短歸結(jié)途徑。它是一種完備的歸結(jié)戰(zhàn)略。寬度優(yōu)先對(duì)大問(wèn)題的歸結(jié)容易產(chǎn)生組合爆炸，但對(duì)小問(wèn)題卻仍是一種比較好的歸結(jié)戰(zhàn)略。歸結(jié)演繹推理的歸結(jié)戰(zhàn)略

-廣度優(yōu)先戰(zhàn)略2023/12/25138支持集戰(zhàn)略是沃斯(Wos)等人在1965年提出的一種歸結(jié)戰(zhàn)略。它要求每一次參與歸結(jié)的兩個(gè)子句中，至少應(yīng)該有一個(gè)是由目的公式的否認(rèn)所得到的子句或它們的后裔。可以證明支持集戰(zhàn)略是完備的，即當(dāng)子句集為不可滿(mǎn)足時(shí)，那么由支持集戰(zhàn)略一定可以歸結(jié)出一個(gè)空子句。也可以把支持集戰(zhàn)略看成是在寬度優(yōu)先戰(zhàn)略中引入了某種限制條件，這種限制條件代表一種啟發(fā)信息，因此有較高的效率歸結(jié)演繹推理的歸結(jié)戰(zhàn)略

-支持集戰(zhàn)略2023/12/25139﹁I(x)∨R(x)I(a)﹁R(y)∨L(y)﹁L(a)R(a)﹁I(x)∨L(x)L(a)L(a)﹁I(a)NIL設(shè)有如下子句集：S={﹁I(x)∨R(x),I(a),﹁R(y)∨L(y),﹁L(a)}其中，﹁I(x)∨R(x)為目的公式的否認(rèn)。用支持集戰(zhàn)略證明S為不可滿(mǎn)足。2023/12/25140各級(jí)歸結(jié)式數(shù)目要比寬度優(yōu)先戰(zhàn)略生成的少但在第二級(jí)還沒(méi)有空子句。就是說(shuō)這種戰(zhàn)略限制了子句集元素的劇增，但會(huì)添加空子句所在的深度。支持集戰(zhàn)略具有逆向推理的含義，由于進(jìn)展