只有一条规则的推理

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
      • 因为推理规则是可靠的（检查真值表）

C1	C2	C1∨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) }不可满足
  

1. 先把能两两归结的原S中的都归结了–>S1
2. 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前向链的完备性证明