【正文】 兩個謂詞公式： E1： P(x,y,z)。 可以證明，如果 E1和 E2可合一，則算法必停止于第（ 3）步。 自然演繹推理方法 肯定后件的錯誤 是指當(dāng) P→ Q為真時，希望通過肯定后件 Q為真來推出前件 P為真。 即 ， 我們先否定邏輯結(jié)論 Q， 再由否定后的邏輯結(jié)論～ Q及前提條件 P出發(fā)推出矛盾 ， 即可證明原問題 。 歸結(jié)推理方法 （ 4） 消去存在量詞 。 定義 由子句構(gòu)成的集合稱為 子句集 。 （ 2） 令 Hi+1=Hi∪ {S中所有的形如 f(t1,… ,tn)的元素 } 其中 f(t1,… ,tn)是出現(xiàn)于 G中的任一函數(shù)符號 ， 而 t1， … ， tn是 Hi中的元素 。 歸結(jié)推理方法 3． H域上的解釋 定義 如果子句集 S的原子集為 A， 則對 A中各元素的真假值的一個具體設(shè)定都是 S的一個 H解釋 。 歸結(jié)推理方法 定理 子句集 S不可滿足的充分必要條件是存在一個有限的不可滿足的基例集 S′ 。 歸結(jié)推理方法 歸結(jié)原理 定義 若 P是原子謂詞公式或原子命題 ， 則稱 P與～ P為 互補文字 。否則轉(zhuǎn) （ 4） 。 從而沒有辦法進行歸結(jié) 。 （ 4） C1的因子 C1σ1與 C2的因子 C2σ2的二元歸結(jié)式 。 證明 首先將 A和～ B化為子句集 (1) ～ P(x,y)∨ ～ Q(y) ∨ R(f(x)) (2) ～ P(x,y)∨ ～ Q(y) ∨ T(x,f(x)) //(1)(2)為 A (3) ～ R(z) (4) P(a， b) (5) Q(b) //(3)(4)(5)為 B 歸結(jié)推理方法 下面進行歸結(jié)： （ 6） ～ P(x,y)∨ ～ Q(y) （ 1） 與 （ 3） 歸結(jié) ， σ={f(x)/z} （ 7） ～ Q(b) （ 4） 與 （ 6） 歸結(jié) ， σ={a/x,b/y} （ 8） NIL（ 空子句 ） （ 5） 與 （ 7） 歸結(jié) 所以 B是 A的邏輯結(jié)論 。 （ 1） 定義謂詞： 設(shè) Father(x,y)表示 x是 y的父親 。 將其否定與 ANSWER作析取 ， 得： G：～ Father(u,Peter)∨ ANSWER(u) 歸結(jié)推理方法 第三步：將上述公式 G化為子句集 S2， 并將 S1和 S2合并到 S。 由于事先并不知道子句集中的哪兩個子句可以進行歸結(jié) ，也不知道通過對哪些子句的歸結(jié)可盡快得到空子句 ， 所以就必須對子句集中的所有子句逐一進行比較 ， 以對所有可能歸結(jié)的子句對進行歸結(jié) ，并將歸結(jié)式加入 S中 ， 再做第二層這樣的歸結(jié) ?? ， 直到產(chǎn)生空子句（ NIL） 為止 。 例如 ， 設(shè)有子句集 ， S={T∨ Q∨ R,～ R,Q,R∨ ～ Q} 其中 T是純文字 ， 因此可將子句 T∨ Q∨ R刪去 ， 只用剩余的子句集進行歸結(jié) ， 不會影響 S的不可滿足性 。 歸結(jié)推理方法 2． 線性歸結(jié)策略 線性歸結(jié)策略對參加歸結(jié)的子句提出如下限制：首先從子句集 S中先取一個稱作 頂子句 的子句 C0開始作歸結(jié)；其次是將歸結(jié)過程中所得到的歸結(jié)式 Ci立即同另一子句 Bi進行歸結(jié) ， 得歸結(jié)式 Ci+1， 而 Bi是原子句集 S中的一個子句或是已經(jīng)歸結(jié)出的某個歸結(jié)式 Cj（ ji） 。 5． 支持集策略 支持集策略對參加歸結(jié)的子句提出如下限制：每一次歸結(jié)時 ， 參加歸結(jié)的兩個子句中至少應(yīng)有一個是由目標(biāo)公式的否定所得到的子句 ， 或者是它們的后裔 。 這有利于朝著空子句的方向前進 ， 因此它有較高的歸結(jié)效率 。 可以從子句集中刪去重言式 。 歸結(jié)推理方法 2． 控制策略的分類 歸結(jié)策略大致可分為兩大類：一類是刪除策略 ， 刪除策略包括：純文字刪除法 、 重言式刪除法 、 包孕刪除法 。 （ 4） ～ Father(u,Peter)∨ ANSWER(u)。 (x)(y)(z)(Brother(x,y)∧ Father(z,x)→ Father(z,y)) F2： John和 Peter是兄弟 。 （ 3） 把問題公式與謂詞 ANSWER構(gòu)成的析取式化為子句集 ， 并把該子句集與 S1合并構(gòu)成子句集 S。 歸結(jié)推理方法 利用歸結(jié)原理進行定理證明 應(yīng)用歸結(jié)原理進行定理證明的步驟如下： 設(shè)要被證明的定理可用謂詞公式表示為如下的形式： A1∧ A2∧ … ∧ An→ B (1) 首先否定結(jié)論 B， 并將否定后的公式～ B與前提公式集組成如下形式的謂詞公式： G= A1∧ A2∧ … ∧ An∧ ～ B (2) 求謂詞公式 G的子句集 S。 定義 設(shè) C1和 C2是沒有相同變元的子句 ， 則下列四種二元歸結(jié)式都叫做 C1和 C2的歸結(jié)式 ， 仍記作 C12。 為了說明的方便 。 如果把C12加入子句集 S后得到新子句集 S1， 則 S1和 S在不可滿足的意義下是等價的 。 歸結(jié)推理方法 必要性： 設(shè)子句集 S不可滿足 ， 由定理 ， S對 H域上的所有解釋均為假 。 證明 充分性 ：若 S在一般域 D上是不可滿足的 ， 必然在 H域上是不可滿足的 ， 從而對 H域上的一切解釋都為假 。 歸結(jié)推理方法 定義 將沒有變元出現(xiàn)的原子 、 文字 、 子句和子句集分別稱作 基原子 、 基文字 、 基子句 和 基子句集 。 但是 ， 在不可滿足的意義下 ， 子句集 SP與 S1∪ S2∪ S3… ∪ Sn是一致的 ， 即 SP不可滿足 ?S1∪ S2∪ S3… ∪ Sn不可滿足 歸結(jié)推理方法 Herbrand理論 1． H域 定義 設(shè)謂詞公式 G的子句集為 S， 則按下述方法構(gòu)造的個體變元域 H。 需要指出的是 ， 由于在化解過程中 ， 消去存在量詞時作了一些替換 ，一般情況下 ， G的 Skolem標(biāo)準(zhǔn)型與 G并不等值 。 例如 ， 如果用 f(x)代替上面前束形范式中的 y即得到 Skolem范式： (? x) (? z)(P(x)∧ F(f(x), z)∧ Q(f(x), z)) Skolem標(biāo)準(zhǔn)型的一般形式是 (? x1)(? x2)… (? xn)M(x1,x2,… ,xn) 其中 ， M(x1,x2,… ,xn)是一個合取范式 ， 稱為 Skolem標(biāo)準(zhǔn)型的母式 。 相關(guān)的例題請參見教材 自然演繹推理方法 演繹推理的特點 參見教材 歸結(jié)推理方法 研究用計算機實現(xiàn)定理證明的機械化 ， 已是人工智能研究的一個重要領(lǐng)域 。 假言三段論的基本形式為 P→Q ， Q→R ?P→R 它表示如果謂詞公式 P→Q 和 Q→R 均為真，則謂詞公式 P→R 也為真。 （ 4） 找出 Wk的不一致集 Dk 。 ? = ? 。 ? 。 ?/x1,t2 定理 Q為 P1， P2， … ， Pn的邏輯結(jié)論 ， 當(dāng)且僅當(dāng) (P1∧ P2∧ … ∧ Pn)∧ ～ Q是不可滿足的 。若對 D上的任何一個解釋， P與 Q的取值都相同，則公式 P和 Q在域D上是 等價的 。 詳細的求解過程參見教材 謂詞邏輯 2． 謂詞公式的永真性 定義 如果謂詞公式 P， 對個體域 D上的任何一個解釋都取得真值 T， 則稱 P在 D上是 永真的 ；如果 P在每個非空個體域上均永真 ， 則稱 P永真 。 （ 2） 若 A是合式公式 ， 則～ A也是合式公式 。 謂詞的語義： 由使用者根據(jù)需要人為地定義 . 謂詞邏輯 謂詞的元數(shù)： 謂詞中包含的個體數(shù)目稱為謂詞的 元數(shù) ，例如 P(x)是一元謂詞， P(x,y)是二元謂詞，而 P(x1,x2,…,x n )則是 n元謂詞。 謂詞 則是用于刻畫個體的性質(zhì) 、 狀態(tài)或個體間的關(guān)系的 。 ?：稱為 “ 雙條件 ” 。 我們一般用 P、 Q、 R、 ? 大寫拉丁