只有一條規則的推理

resolution(消解，歸結）

• CNF（conjunction normal form合取范式
  • $（A\vee B)\wedge (B\vee C)$
  • 任何邏輯式都可轉化為語義等價的CNF
• resolution消解（推理規則）
  • 完備的
  • 可靠的
    
    complementary literal:互補文字
    eg:A和?A

resolution是完備的、可靠的

• 可靠性：|- --> |=
  • 歸結的過程是可靠的
  • 歸結過程：C1、C2中有互補文字==》C1∨C2
    • 已知C1,C2 |- C1∨C2
    • 證明C1,C2 |= C1∨C2
      • 因為推理規則是可靠的（檢查真值表）

C1C2C1∨C2

false	false	false
true	false	true
false	true	true
true	true	true

• 完備性：

  • 已知C1,C2 |= C1∨C2
  • 證明C1,C2 |- C1∨C2
  • RC(S)–歸結閉集 resolution closure–所有S歸結出來的都在RC(S)中=PL-Resolution(KB,$\alpha$)的最終clauses
    • S={KB,?$\alpha$}
      • KB |=$\alpha$<>KB∧ ?$\alpha$不可滿足（永假）<=>S不可滿足
  • ground resolution theorem:S不可滿足==>RC(S)中包含空子句
    • 證明：從逆否命題入手:S可滿足<==RC(S)中不包含空子句
  • 因為RC(S)是有限的，所以PL-Resolution(KB,$\alpha$)總是可以終止的
  • PL-Resolution(KB,$\alpha$)的終止條件是clauses中包含空子句

• ground resolution theorem:S不可滿足==>RC(S)中包含空子句

  • 證明：從逆否命題入手:RC(S)中不包含空子句==>S可滿足

• 所以不會有子句被指派為false==>也就是，S歸結出來的所有子句均為真===>S可滿足的（第二個反證）
  

1。轉化為CNF

• 多項式時間復雜度：存在可以多項式時間解決這個問題的算法

2.歸結算法PL-Resolution(KB,$\alpha$)

• 證明 $KB\wedge \alpha$
  • clauses:$KB\wedge \alpha$的子句集
  • 子句集中如果有可以消解的就消解了（遞歸），將消解后的句子加入new
  • 如果new是clauses的子句則消解失敗
  • 否則clauses<–clauses U new
  • 若最后得到了一個空集，則成功
    

歸結策略—search（在計算機中實現）

廣度優先的歸結策略

• 證明S={﹁I(x)∨R(x), I(a), ﹁R(y)∨L(y), ﹁L(a) }不可滿足
  

先把能兩兩歸結的原S中的都歸結了–>S1

S1+S–>S2

Modus ponens、horn

• 時間復雜度：線性，比歸結原理的時間復雜度低

• 給子句加限制–>更高效

  • 縮小命題子句的表達范圍，以換取更好的推理時間效率

• definity 子句：有且只有一個正文字

• horn子句：析取的文字中，之多只能有一個為正

  • 是閉合的：
    • horn子句歸結后還是horn子句
  • eg:
    • true=>A
      • ?true∨ A==>falseV A(是horn
    • （A∧B∧C)=>D
      • ?（A∧B∧C)∨D
      • ==>?A∨?B∨?C∨D

• 前向后向鏈

• horn form

  • KB：是horn子句的集合
  • horn子句：
    • 命題符號eg:A
    • （A∧B∧C)=>D

• 肯定式推理modus ponens
  
  可以被前向鏈、后向鏈使用

• why會非常高效？

  • 在歸結原理中，需要n次才能得到結果
  • horn一次就可以得到結果

前向鏈forward chaining

• KB是圖中的horn子句
• 將他們的結論加入KB，知道最終結果被找到
  
  agenda=是單個文字的隊列
  count=最初的前提數目
• 初：agenda=[A,B]
• A=pop(agenda)
• 令A=true
• 帶入到各式中，并重新計算count
• count為0的加入agenda
• 重復直至隊列首位為Q

紅色的是count–這樣算也可

• FC前向鏈：是數據驅動的，推出來的不一定需要的目標

• 后項鏈是結論驅動的

• 后向鏈比前向鏈高效

• 優點

  • 命題邏輯是聲明性的:語法片段對應于事實。
  • 命題邏輯允許部分/析取/否定信息(與大多數數據結構和數據庫不同)。
  • 命題邏輯是組合邏輯
  • 命題邏輯中的意義是上下文無關的(不像自然語言，意義依賴于上下文)

• 缺點

  • 命題邏輯的表達能力非常有限。不能說“小坑在相鄰的方格里產生微風”，除非給每個方格寫一個句子。

FC前向鏈的完備性證明

總結

以上是生活随笔為你收集整理的国科大高级人工智能8-归结原理和horn子句的全部內容，希望文章能夠幫你解決所遇到的問題。

如果覺得生活随笔網站內容還不錯，歡迎將生活随笔推薦給好友。