【正文】 ?… ? Ln 子句集 SA={A1, A2,…, A n } ? 無 ? 型前束合取范式 北京航空航天大學軟件開發(fā)環(huán)境國家重點實驗室 Slide 18 子句的 標準范式 ? 無 ? 型前束合取范式 : （ Q1x1） (Q2x2） … （ Qnxn） M 其中， Qi：全稱量詞； xi：變元 母式： M = (A11? A12?… ? A1n ) ? … ? (Am1? Am2?… ? Aml ) 是 合取范式 ， 其中 , Aij是文字。 設 : A,B是合式謂詞公式，則 ? A， A?B， A?B， A?B, (?x) A 是合式謂詞公式。 ., brother2(x, y)。 ? 一階 邏輯滿足形式化表達和處理要求 ： ? 類自然語言的形式化的符號語言 （ 謂詞公式描述 ） ? 強有力的推理方法（ 公理化推理方法、歸結(jié)法 ）； ? 堅實的理論證明基礎（ 語義模型、推理的可靠性、完備性研究等 ）。 Fn, gm, …..。 變元 : x,y,….。 ?（ 1）指定一個非空集合 DI，稱為 I 的論域； ?（ 2）對于每個常元 a，指定 DI 中的一個元素 aI； ?（ 3）對于每個 n元函數(shù)符號 f，指定 DI上的一個 n元運算符 fI ?（ 4）對于每個 n元謂詞符號 P，指定 DI上的一個 n 元謂詞 PI 北京航空航天大學軟件開發(fā)環(huán)境國家重點實驗室 Slide 14 解釋與賦值 ? 賦值定義 : ?設 I 是一個解釋，將所有 變元 組成的集合映射到論域 DI 的函數(shù)稱為 I 中的賦值 v。 ? 推論： 設 C 是 C1 和 C2 的歸結(jié)式，則子句集 S = ? C1， C2 ， … Cn ? 與 子句集 S1 = ? C， C1，C2 ， … Cn ? 的 不可滿足性 等價。 例： 設 s = { A/x, B/y } ? = {B/y }， S’ = {A/x}, 有： S = ? S’ 。 {Ei}={P(f(x,g(z)),h(A)),P(f(x,y),z)} 北京航空航天大學軟件開發(fā)環(huán)境國家重點實驗室 Slide 44 謂詞 歸結(jié)證明系統(tǒng)的相關(guān)技術(shù) ? 合一匹配算法 ? 一階謂詞歸結(jié)原理 ? 歸結(jié)證明系統(tǒng)的基本推理算法 ? 歸結(jié)證明系統(tǒng)的推理策略 北京航空航天大學軟件開發(fā)環(huán)境國家重點實驗室 Slide 45 一階謂詞歸結(jié)原理 ? 歸結(jié)定義： 設 C1,C2是任意的兩個 謂詞 子句 ，其中， C1 = L1 ? C1’ , C2 = L2 ? C2’ ， L1, L2是 可化為 互補文字的兩個原子謂詞公式 ,（即二者間存在最一般合一者mgu ? ）。 ? 第 i級： Si 1中所有可能歸結(jié)的子句對進行歸結(jié)，產(chǎn)生全部歸結(jié)式， 將其加到歸結(jié)子句集 Si 1中獲新的歸結(jié)子句集 Si = Si 1 ? ?第 i 級歸結(jié)式 ?。 為了加快歸結(jié)進度， 因此， 有 單元歸結(jié)策略。 北京航空航天大學軟件開發(fā)環(huán)境國家重點實驗室 Slide 65 線性歸結(jié)策略（ 2） 線性歸結(jié)例： 設 S=?A? B, ? A ? B, A ? ? B, ? A ? ? B? ? ? ? B A ? ? B A ? A ? ? B ? B B 歸結(jié)策略特點： ? 當 C0 或 B0 之一等于 ? ? 時，線性歸結(jié)為 支持集策略 ； ? 與單元歸結(jié)策略類似，優(yōu)先選擇較短的母子句進行歸結(jié)。 ? F3: Tail(sid)。 {Ei}={P(f(x,g(z)),h(A)),P(f(x,y),z)} 北京航空航天大學軟件開發(fā)環(huán)境國家重點實驗室 Slide 78 演講完畢，謝謝觀看！ 。 R2: Kind(s) ? ? Barks(s) ? ? Afraid(x,s)。 北京航空航天大學軟件開發(fā)環(huán)境國家重點實驗室 Slide 66 利用 線性歸結(jié)策略 求證下列公式 永真 : (?x)(P(x) ? (Q(A) ? Q(B))) ? (? x)(P(x) ?Q(x)) 習題： 北京航空航天大學軟件開發(fā)環(huán)境國家重點實驗室 Slide 67 基于邏輯的 應用系統(tǒng) ?基于規(guī)則的演繹推理系統(tǒng) 北京航空航天大學軟件開發(fā)環(huán)境國家重點實驗室 Slide 68 基于規(guī)則的演繹推理系統(tǒng) 問題提出： 因此，有： 基于規(guī)則的演繹推理系統(tǒng) ：直接根據(jù)問題領域的事實和規(guī)則，證明某目標公式是否成立，而不是先將公式化成子句形式，用歸結(jié)反演方法證明。 北京航空航天大學軟件開發(fā)環(huán)境國家重點實驗室 Slide 62 推理策略 實例 單元歸結(jié)策略（ 1） P ? 歸結(jié)策略特點： ? 此策略可縮短歸結(jié)過程，能大大提高搜索效率。 北京航空航天大學軟件開發(fā)環(huán)境國家重點實驗室 Slide 58 推理策略分析 改進（ 1） 策略分析： 由于前提公式集中并無矛盾，推理反駁是由待證結(jié)論的否定式加入引起的。 求證 : ?有些很機靈的東西不會朗讀 一階謂詞描述： ?(?x)(R(x) ? L(x)) ?(?x)(D(x) ? ? L(x)) ?(? x)(D(x) ? I(x)) 求證： w =(? x)(I(x) ? ? R(x))) 設原子謂詞公式： R(x)： x 會朗讀； L(x)： x 識字 D(x)： x 是海豚； I(x)： x 機靈 ?W = ? (? x)(I(x) ? ? R(x)) = (? x) ? (I(x) ? ? R(x)) = (? x) ?I(z) ? R(z) 北京航空航天大學軟件開發(fā)環(huán)境國家重點實驗室 Slide 50 一階謂詞歸結(jié) 證明系統(tǒng) 應用實例 （ 2） 子句集： S0 = ?? R(x)? L(x), ? D(y)?? L(y), D(A), I(A), ?I(z)? R(z)? 求證： S0 |= 北京航空航天大學軟件開發(fā)環(huán)境國家重點實驗室 Slide 51 一階謂詞歸結(jié)證明系統(tǒng) 應用實例 （ 3） S0 = ?① ? R(x)? L(x), ② ? D(y)?? L(y), ③ D(A), ④ I(A), ⑤ ?I(z)? R(z)? A/y A/z A/x ? D(y)? ? L(y) D(A) ② ③ ?I(z)? R(z) I(A) ④ ⑤ ? R(x)? L(x) ⑦ ① L(A) ⑥ ⑧ 空 ? L(A) ⑥ R(A) ⑦ 北京航空航天大學軟件開發(fā)環(huán)境國家重點實驗室 Slide 52 謂詞 歸結(jié)證明系統(tǒng)的相關(guān)技術(shù) ? 合一匹配算法 ? 一階謂詞歸結(jié)原理 ? 歸結(jié)反演系統(tǒng)的基本算法 ? 歸結(jié)證明系統(tǒng)的推理策略 北京航空航天大學軟件開發(fā)環(huán)境國家重點實驗室 Slide 53 歸結(jié)證明系統(tǒng)的 推理策略 ?搜索策略的 完備性 如果給定問題的子句集存在矛盾，便可以通過運用某種歸結(jié)搜索策略 ,最終構(gòu)造出一棵以 結(jié)尾的歸結(jié)反演樹，稱此歸結(jié)搜索策略是完備的。 北京航空航天大學軟件開發(fā)環(huán)境國家重點實驗室 Slide 40 合一匹配算法： ? 分歧