【正文】 證明 子句集 S的不可滿足性 與證明 合適公式永真性 類似p 由于個體 論域 的任意性和 解釋 個數(shù)的無限性，使得證明工作 十分困難 。星期六 68歸結(jié)演繹推理歸結(jié)演繹推理1） H域和海伯倫定理p 子句和子句集合適公式 F 合取范式 子句集 S合適公式 F永假子句集 S的不可滿足性充分必要條件重要性質(zhì)S的不可滿足性任意論域 D上的任意解釋 I,S中都 至少 有一個 子句 真值為 F2023/2/27P(A) ?P(f(A,y2))∨ ?Q(A,z2)∨ P(z2,g(z2))?(?x){P(x)?{(?y)[P(y)P(y1)∨ ?Q(A,z1)∨ P(z1,g(z1))]S后， F和 S在永假性上是等價的2023/2/27更換變量名稱，使一個變量符號不出現(xiàn)在一個以上的子句中。反復(fù)代替的結(jié)果，最后得到一個有限集，其中每個公式是文字的析取。 ∧全稱量詞的次序也不重要了。{A∨ B}∧ {A∨ C}這種母式叫做合取范式。(?x)(?y){P(x)∨ 前束形公式由全稱量詞串組成的 前綴 和不含量詞的 母式 組成。星期六 66現(xiàn)在已不存在任何存在量詞，而且每個全稱量詞都有自己的變量，把所有全稱量詞移到公式的左邊，并使每個量詞的轄域包括這個量詞后面公式的整個部分。例如，（ ?x） P（ x）化為 P（ A），其中常量符號 A用來表示我們知道的存在實體。（ ?y） P[g（ y）， y]Skolem函數(shù)的變量是由那些全稱量詞所約束的全稱量詞量化變量，這些全稱量詞的轄域包括要被消去的存在量詞的轄域在內(nèi)。這種函數(shù)就是 Skolem函數(shù)。 星期六 65子句：文字的析取組成的公式。量詞有其自己唯一的啞元。啞元（虛構(gòu)變量），它可以在該轄域內(nèi)處處統(tǒng)一的被另一個沒有出現(xiàn)過的任意變量所代替，而不改變公式的真值。在任一量詞轄域內(nèi)，受該量詞約束的變量為 A}代替 ~（ ?x） A代替 ~（ A∨ B）以 A代替 ~（ ~A）以 (?x){~如以 ~A∨ ~B ★2023/2/27(?z)[P(y)∨ ?Q(A,z)∨ P(z,g(z))],(?y)星期六 63歸結(jié)演繹推理歸結(jié)演繹推理1） H域和海伯倫定理p 子句和子句集n 子句中的變量都是 ?的約束變量{(?y)∧(?y)∧(?y)Q(x)(?y)(?x)P(x)Q(x)][P(x)星期六 62歸結(jié)演繹推理歸結(jié)演繹推理1） H域和海伯倫定理p 子句和子句集n 子句 —— 僅由 文字 的 析取 ∨ 構(gòu)成的合適公式n 合取范式表示為 子句集 ，子句間隱含具有 合取關(guān)系(?y)；n 合取范式 表示為 子句集 ，子句間隱含 合取 ∧ 關(guān)系p子句集 {W1,W2,…, Wn}2023/2/27 ∧ WnpWi=Li1∨ Li2∨ …星期六 60歸結(jié)演繹推理歸結(jié)演繹推理1） H域和海伯倫定理（了解）p 子句和子句集n 子句 —— 僅由 文字 的 析取 ∨ 構(gòu)成的合適公式pWi=Li1∨ Li2∨ …星期六 59歸結(jié)演繹推理歸結(jié)演繹推理p 海伯倫（ Herbrand）n 提出的 H域（海伯倫域） 和 海伯倫定理 ；n 為 自動定理證明 奠定了理論基礎(chǔ)；p 魯賓遜（ Robinson）n 提出的 歸結(jié)原理 ；n 使 自動定理證明 成為可能。 ∪ {?W}是一個矛盾集。F2,…,F n都是合適公式，表示 公理 或 事實 ；n W是合適公式，表示 待證明的定理 ，稱為 目標(biāo)公式 ；p 證明的方法可分兩大類：n 演繹法p直接證明 F1∧ F2∧ … ∧ Fn?W為 永真 ；n 反證法p間接證明 ?(F1∧ F2∧ … ∧ Fn?W)為 永假 ；p證明 F1∧ F2∧ … ∧ Fn歸結(jié)演繹推理歸結(jié)演繹推理p 自動定理證明一般表示形式為：p F1∧ F2∧ … ∧ Fn?Wn F1,星期六 57p 合取范式的標(biāo)準(zhǔn)化過程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))]}} 完成標(biāo)準(zhǔn)化過程！2023/2/27星期六 55p 合取范式的標(biāo)準(zhǔn)化過程n 例、化簡合適公式{P(A)∧{(?y)[P(y)∧ ?P(f(A,y))]∨ (?z)[?Q(A,z)∨ P(z,g(z))]}}⑥ 全稱量詞前束化(?y)(?z){P(A)∧{[P(y)∧ ?P(f(A,y))]∨ [?Q(A,z)∨ P(z,g(z))]}}2023/2/27星期六 53p 合取范式的標(biāo)準(zhǔn)化過程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/2/27?P(f(x,y))]∧ ?(?y)(?w)[Q(x,y)?P(y,w)]}}② 消去蘊(yùn)涵符號?(?x){?P(x)∨{(?y)[?P(y)∨ P(f(x,y))]∧ ?(?y)(?w)[?Q(x,y)∨ P(y,w)]}}2023/2/27?P(f(x,y))]∧ ?(?y)(?w)[Q(x,y)?P(y,w)]}}2023/2/27R)2023/2/27(PQ)(PR)(Qp ⑧ 把母式轉(zhuǎn)化為 合取范式n 分配律 ： P星期六 49p 合取范式的標(biāo)準(zhǔn)化過程p ⑥ 全稱量詞前束化n 經(jīng)過 “ ④ 變量換名 ” 后，所有量詞的約束變量均有不同的名字；n 只要簡單地將 ?移到合適公式的最前面；n 約束變量的作用范圍不會變化。Skolem變換 不是等價變換，但變換前后的值永假性保持不變 。所使用的常量符號必須是 新的 ，它未曾在公式其他地方使用過。 在消去存在量詞的過程中，需要用到 Skolem函數(shù)或Skolem常量?！?P(z,A)] 前兩種叫 Skolem函數(shù)，第三種叫 Skolem常量2023/2/27∨ P(z,w)]p用 任意常量 A取代約束變量 w，消去存在量詞 ?wp(?z)∨ P(z,g(z))]n ?在 多個 ?的轄域內(nèi)p (?x)(?y)(?z)(?w)P(x,y,z,w)p 用多元函數(shù) g(x,y,z)來取代約束變量 w，消去存在量詞 ?w；p (?x)(?y)(?z)P(x,y,z,g(x,y,z))n ?在 ?的轄域外p(?w)(?z)星期六 47p 合取范式的標(biāo)準(zhǔn)化過程p ⑤ 消去存在量詞（ Skolem變換 ）n ?在 ?的轄域內(nèi)p (?z)(?w)[?Q(x,z)標(biāo)準(zhǔn)化而得到（ ?x） {p(x)=（ ?y） Q（ y） }(?x){p(x)=（ ?x） Q（ x） }n 例， (?x)P(x)(?P(x))?Pn 量詞否定：p ?(?x)?Qn 雙重否定： ?(?P)P?∧ ∧ ?Q)星期六 46p 合取范式的標(biāo)準(zhǔn)化過程p ③ 內(nèi)移否定符號n 使否定只出現(xiàn)在原子謂詞公式前，構(gòu)成 否定文字 ；n 狄 .摩根定律：p ?(PP(y)。?Q(x,y)P(y)Q(x,y)∨ ??星期六 45p 合取范式的標(biāo)準(zhǔn)化過程p ① 消去多余的量詞（很少出現(xiàn)）n 若 一個量詞的轄域內(nèi)并未出現(xiàn)量詞的約束變量 ，則該量詞是多余的，應(yīng)該刪除；n 例， (?x)P(y)，則 (?x)可以消去，得到 P(y)；n 正常情況下，合適公式中不應(yīng)出現(xiàn)多余的量詞。n 轉(zhuǎn)化步驟沒有嚴(yán)格的規(guī)定n 較合理的化簡過程，分為 8步：p① 消去多余的量詞（很少出現(xiàn)）；p② 消去蘊(yùn)涵符號；p③ 減少否定的轄域（內(nèi)移否定符號）；p④ 變量標(biāo)準(zhǔn)化（變量換名）；p⑤ 消去存在量詞 (Skolem變換 ) ；p⑥ 全稱量詞前束化（化為前束形）；p⑦ 消去全稱量詞；p⑧ 把 母式 轉(zhuǎn)化為 合取范式 。 ∨ Lim(i=1,2,…,n)pLij=Pij|?Pij:文字（ Literal） ，是 謂詞公式 Pij或 其取反2023/2/27—— 母式，不包括任何量詞；p Qixi——Q i可以是 量詞 符號 ?或 ?； xi是量詞的 約束變量(i=1,2,…,k)n 歸結(jié)反演 —— 要求 M標(biāo)準(zhǔn)化為 合取范式 ，定義如下：pM=W1∧ W2∧ …星期六 43合適公式的標(biāo)準(zhǔn)化合適公式的標(biāo)準(zhǔn)化 ★p 標(biāo)準(zhǔn)化需求n 常見的基于謂詞演算的推理： 歸結(jié)反演 、 (正向 /逆向 )演繹推理p 要求以 量詞前束范式 來表示合適公式n 量詞前束范式 形式如下：p (Q1x1) 從一階邏輯的公式變換到 Skolem標(biāo)準(zhǔn)型 不是等值變換，因為 Skolem標(biāo)準(zhǔn)型與原公式不等值。星期六 42Skolem標(biāo)準(zhǔn)型p 通過變換 消去存在量詞 所得到的公式稱為 Skolem標(biāo)準(zhǔn)型 ，而拿來代替存在量詞的變量的函數(shù)稱Skolem函數(shù) 。 星期六 41一階邏輯公式所對應(yīng)的 Skolem標(biāo)準(zhǔn)型基于如下思想來構(gòu)造：1. 一階邏輯的一個公式被變換為前束范式。反演法利用了一個標(biāo)準(zhǔn)型，這個標(biāo)準(zhǔn)型就是 Skolem標(biāo)準(zhǔn)型。星期六 40史柯倫標(biāo)準(zhǔn)型及其構(gòu)造思想p 史柯倫（ Skolem）標(biāo)準(zhǔn)型 ：海伯倫（ Herbrand）定理是歸結(jié)原理的基礎(chǔ)。P(x， z)∨ ~P(y， z))∨ (?u)Q(x， y， u)??x)(?y)(?z)(?u)(~星期六 38前束范式例 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/2/27(Q2x2)…(Q kxk)M，其中p M星期六 36合適公式的性質(zhì)　 (?x)[P(x)∧Q(x)] ? (?x)P(x)∧( ?x)Q(x)(?x） [P(x)∨Q(x)] ?（ ?x） P(x)∨( ?x)Q(x)　　　　 (?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/2/27(?x)P(x) ?（ ?x)(172。(?x)P(x) ? (?x)(172。 Q? 172。星期六 35合適公式的性質(zhì)6. 結(jié)合律 　 　 (P∧Q)∧R ? P∧(Q∧R ）　　 (P∨Q)∨R ? P∨ （ Q∨R ） 7. 逆否律 P∨ 172。Q 172。(P∨Q) ? 172。P) ? P 2. 蘊(yùn)涵式轉(zhuǎn)化 P?Q ? 172。 172。星期六 34合適公式的性質(zhì)合適公式等價關(guān)系 : 1. 否定之否定 n 連詞優(yōu)先級別 是 ?， ∧ 、 ∨ ， ?、 ?，但可通過 括號 改變優(yōu)先級。)函數(shù)名進(jìn)行了量化；n P(x,Q(y))參數(shù)項是謂詞公式；2023/2/27星期六 32p 一階謂詞邏輯n 定義： 若限定 不允許 對 謂詞 和 函數(shù)名 進(jìn)行 量化 處理，且 參數(shù)項 不能是 謂詞公式 ，則這樣的謂詞邏輯是 一階 的。真值為 T。都有 P(x)真值為 T。條條大路通羅馬Mary給每個人一本書Mary給每人某個同樣的東西量詞可以嵌套使用可以有不受量詞約束的變量2023/2/27n 存在量詞 ?p符號 (?x)P(x)：來表示某個論域中 至少存在一個 個體 x，使 P(x)星期六 30p 連詞和量詞 —— （ 2）量詞n 全稱量詞 ?p符號 (?x)P(x)：表示對于某個論域中的 所有（任意一個） 個體 x,pLead(Road1,Roma)pLead(Road2,Roma)……n 謂詞邏輯 中引入 變量 和對變量進(jìn)行約束的 量詞 。星期六 29p 連詞和量詞n 命題 —— 不包含 變量 的 謂詞公式 和 邏輯語句 ；n 命題邏輯 —— 基于 命題 的 謂詞邏輯 稱為 命題邏輯 ， 命題邏輯是謂詞邏輯的子集 。n 復(fù)合謂詞公式也稱為 邏輯語句 。2023/2/27（蘊(yùn)涵）連接 謂詞公式 產(chǎn)生 蘊(yùn)涵式 ；左部稱為 前項 ，右部稱為 后項 。（與）連接 謂詞公式 ，稱為 合取 ；產(chǎn)生的 邏輯語句 稱為 合取式 ，每個成分成為 合取項。n 復(fù)合謂詞公式 也稱為 邏輯語句 。2023/2/27星期六 26回顧謂詞邏輯表示法回顧謂詞邏輯表示