【正文】 出現(xiàn)在公式的最前面 ，且它的轄域一直延伸到公式之末 ， 同時公式中不出現(xiàn)連接詞 → 及 ? ，這種形式的公式稱作前束形范式 。 歸結推理方法 將謂詞公式 G化為 Skolem標準型的步驟如下： （ 1） 消去謂詞公式 G中的蘊涵 （ → ） 和雙條件符號（ ? ） ， 以～ A∨ B代替 A→ B， 以 (A∧ B)∨ (～ A∧ ～ B)替換A?B。 這里分兩種情況 ， 一種情況是存在量詞不出現(xiàn)在全稱量詞的轄域內(nèi) ， 此時 ， 只要用一個新的個體常量替換該存在量詞約束的變元 ， 就可以消去存在量詞；另一種情況是 ， 存在量詞位于一個或多個全稱量詞的轄域內(nèi) ， 這時需要用一個 Skolem函數(shù)替換存在量詞而將其消去 。 歸結推理方法 2． 子句與子句集 定義 不含有任何連接詞的謂詞公式叫 原子公式 ， 簡稱原子 ， 而原子或原子的否定統(tǒng)稱 文字 。 歸結推理方法 3． 不可滿足意義下的一致性 定理 設有謂詞公式 G， 而其相應的子句集為 S，則 G是不可滿足的充分必要條件是 S是不可滿足的 。 稱為公式 G或子句集 S的 Herbrand域 ， 簡稱 H域 。i=0， 1， 2， … 。 定義 當子句集 S中的某個子句 C中的所有變元符號均以其 H域中的元素替換時 ， 所得到的基子句稱作 C的一個 基例 。 可以證明 ， 在給定域 D上的任一個解釋 I， 總能在 H域上構造一個解釋 I*與之對應 ， 使得如果 D域上的解釋能滿足子句集S， 則在 H域的解釋 I*也能滿足 S（ 即若 S|I=T， 就有 S|I*=T） 。 必要性 ：若 S在任一 H解釋 I*下均為假 ， 必然會使 S在 D域上的每一個解釋為假 。 該定理稱為 Herbrand定理 ， 下面給出它的簡要證明 。 這樣 ， 就至少會存在一個 S中的某子句Ci的基例 Ci′ 為假 。 1． 命題邏輯中的歸結原理 ? 歸結與歸結式 定義 設 C1與 C2是子句集中的任意兩個子句 ， 如果 C1中的文字 L1與C2中的文字 L2互補 ， 則從 C1和 C2中可以分別消去 L1和 L2， 并將二子句中余下的部分做析取構成一個新的子句 C12， 稱這一過程為 歸結 ， 所得到的子句 C12稱為 C1和 C2的 歸結式 ， 而稱 C1和 C2為 C12的 親本子句 。 即： S是不可滿足的 = S1是不可滿足的 歸結推理過程 子句集 S不可滿足性的推理過程如下： (1) 對子句集 S中的各子句間使用歸結推理規(guī)則 。 (4) 置 S=S′， 轉步驟 （ 1） 。 將 Ciσ和 Liσ寫成集合 形式 ， 如 P(x)∨ ～ Q(y)改寫為 {P(x),～ Q(y)}。 （ 2） 在求歸結式時 ， 不能同時消去兩個互補文字對 ， 消去兩個互補文字對所得的結果不是兩個親本子句的邏輯推論 。 （ 1） C1與 C2的二元歸結式 。 歸結推理方法 例 設 C1=～ P(a)∨ Q(x)∨ R(x)， C2 =P(y)∨ ～ Q(b)， 求其二元歸結式 。 (3) 應用歸結原理 ， 證明子句集 S的不可滿足性 ， 從而證明謂詞公式 G的不可滿足性 。 歸結推理方法 應用歸結原理進行問題求解 下面是利用歸結原理求取問題答案的步驟： （ 1） 把已知前提條件用謂詞公式表示出來 ， 并化成相應的子句集 ， 設該子句集的名字為 S1。 歸結推理方法 （ 4） 對子句集 S應用謂詞歸結原理進行歸結 ， 在歸結的過程中 ， 通過合一置換 ， 改變 ANSWER中的變元 。 Brother(x,y)表示 x和 y是兄弟 。 Brother(John,Peter) F3： John的父親是 David。 S2 ={～ Father(u,Peter)∨ ANSWER(u)} S= S1∪ S2 將 S中各子句列出如下： （ 1） ～ Brother(x,y)∨ ～ Father(z,x)∨ Father(z,y)。 歸結推理方法 第四步：應用歸結原理進行歸結 （ 5） ～ Brother(John,y)∨ Father(David,y) （ 1） 與 （ 3） 歸結 σ={David/z,John/x} （ 6） ～ Brother(John,Peter)∨ ANSWER(David) （ 4） 與 （ 5） 歸結 σ={David/u,Peter/y} （ 7） ANSWER(David) （ 2） 與 （ 6） 歸結 第五步：得到了歸結式 ANSWER(David)， 答案即在其中 ， 所以u=David。 這是一種盲目全面的歸結 ， 其結果是產(chǎn)生大量的不必要的歸結式 ， 況且這種不必要的歸結式在下一輪歸結時 ， 會以冪次方的增長速度快速增長 ， 從而產(chǎn)生組合爆炸 。另一類是限制策略 ， 限制策略主要是通過對參加歸結的子句進行種種限制 ， 盡可能地減小歸結的盲目性 ， 使其盡快歸結出空子句 。 歸結推理方法 ? 重言式刪除法 如果一個子句中同時包含互補文字時 ， 則稱該子句為 重言式 。 ? 包孕刪除法 設有子句 C1和 C2， 如果存在一個置換 σ， 使得 C1σ?C2， 則稱 C1包孕于C2。 歸結推理方法 3． 單文字 （ 單元 ） 歸結策略 如果一個子句只包含一個文字 ， 則稱該子句為 單文字子句 或 單元子句 。 但是 ， 這種歸結策略是不完備的 。 演講完畢，謝謝觀看！ 。 歸結推理方法 4． 輸入歸結策略 輸入歸結策略對參加歸結的子句有如下限制：參加歸結的兩個子句中 ， 必須至少有一個子句是初始子句集中的子句 。 用單文字歸結策略時 ， 歸結式將比親本子句含有較少的文字 。 可從子句集中刪去那些被包孕的子句 。 重言式是取值為永真的子句 。 歸結推理方法 歸結控制策略及其應用舉例 1． 刪除策略 ? 純文字刪除法 如果文字 L出現(xiàn)在 S中 ， 而～ L不出現(xiàn)于 S中 ， 便說 L為 S的 純文字 。 在解決上述問題的過程中 ， 人們研究出了許多歸結策略 。 歸結推理方法 歸結過程的控制策略 引入控制策略 1． 引入控制策略的原因 對子句集 S進行歸結時 ， 首先要從子句集中找出可進行歸結的一對子句進行歸結 。 （ 3） Father(David,John)。 設 Peter的父親是 u， 則有： Father(u,Peter)。 F1 ：任何兄弟都有同一個父親 。 歸結推理方法 例 任何兄弟都有同一個父親 ， John和 Peter是兄弟 ， 且John的父親是 David， 問 Peter的父親是誰 ？ 解 第一步：將已知條件用謂詞公式表示出來 ， 并化成子句集 ， 那么要先定義謂詞 。 謂詞 ANSWER是一個專為求解問題而設置的謂詞 ， 其變量必須與問題公式的變量完全一致 。 歸結推理方法 例 已知： A: (?x)((? y)(P(x,y)∧ Q(y))→ (? y)(R(y)∧ T(x,y))) B: ～ (? x)R(x)→ (? x)(? y)(P(x,y)→ ～ Q(y)) 求證： B是 A的邏輯結論 。 即若子句集是不可滿足的 ， 則必存在一個從該子句集到空子句的歸結推理過程；反之 ， 若從子句集到空子句存在一個歸結推理過程 ， 則該子句集必是不可滿足的 。 （ 3） C1與 C2的因子 C2σ2的二元歸結式 。 歸結推理方法 應用因子的概念 ， 可對謂詞邏輯中的歸結原理定義如下 。 歸結推理方法 在謂詞邏輯中 ， 對子句進行歸結推理時 ， 要注意以下幾個問題： （ 1） 若被歸結的子句 C1 和 C2中具有相同的變元時 ， 需要將其中一個子句的變元更名 ， 否則可能無法做合一置換 。 定義 設 C1和 C2是兩個沒有相同變元的子句 ， L1 和 L