只有一条规则的推理

resolution(消解，归结）

CNF（conjunction normal form合取范式
- （A∨B)∧(B∨C)（A∨B)∧(B∨C)（A∨B)∧(B∨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∧αKB∧ \alphaKB∧α
- clauses:KB∧αKB∧ \alphaKB∧α的子句集
- 子句集中如果有可以消解的就消解了（递归），将消解后的句子加入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子句相关推荐

国科大高级人工智能2020-2021年期末试题回顾
国科大高级人工智能2020-2021年期末试题回顾题型选择题简答题应用题附件题型题型没有变,仍然为选择题(20道,每道1分),简答题(3道,每道10分),综合应用题(3道,15,15,2 ...
国科大高级人工智能-总结
文章目录 1.概论 2. 搜索 A\*最优性三个传教士与野人 3.神经网络 RBM DBN DBM hopfield比较结构及特性逐层贪婪训练与CD BP GAN 4.逻辑一个永远无法归结结束 ...
国科大高级人工智能10-强化学习（多臂赌博机、贝尔曼）
文章目录多臂赌博机Multi-armed bandit(无状态) 马尔科夫决策过程MDP(markov decision process 1.动态规划蒙特卡罗方法--不知道环境完整模型情况下 2. ...
国科大高级人工智能7-命题逻辑
文章目录命题逻辑(语法Syntax) 由枚举推理(inference by enumeration 区别 deduction(形式推演,演绎) 作业(定理证明) logics:逻辑,表达信息的形式语 ...
国科大高级人工智能6-GAN
文章目录生成式模型的基础:极大似然估计 GANs 最终版本问题非饱和博弈 DCGAN 不同类型的GAN conditional GAN 无监督条件GAN--cycle GAN 对抗学习 http ...
国科大高级人工智能笔记1-搜索
1.搜索问题搜索问题--对原问题的建模构成: 状态空间包含环境中每一个细节搜索状态:只保留行动需要的细节后继函数行动,消耗初始状态和目标测试解: 一个行动序列,将初始状态–>目标 ...
国科大 - 高级人工智能（沈华伟等）- 期末复习 - 试卷
历年考点 2016 2017 2018 2019 2020 简答题蚁群.粒子蚁群.粒子蚁群.粒子蚁群.粒子简答题 A* 最优性 BP GAN 感知机 BP BP 激活函数简答题语义网络 ...
国科大高级人工智能12-博弈
这里写自定义目录标题欢迎使用Markdown编辑器新的改变功能快捷键合理的创建标题,有助于目录的生成如何改变文本的样式插入链接与图片如何插入一段漂亮的代码片生成一个适合你的列表创建一 ...
国科大高级人工智能9-模糊数学和遗传算法
文章目录 1.模糊计算笛卡尔积.关系模糊集连续的隶属度函数运算 2.evolution 遗传算法 1.模糊计算 why模糊取得精确数据不可能或很困难没有必要获取精确数据模糊性概念:对象从 ...

国科大高级人工智能8-归结原理和horn子句

resolution(消解，归结）

resolution是完备的、可靠的

1。转化为CNF

2.归结算法PL-Resolution(KB,α\alphaα)

归结策略—search（在计算机中实现）

广度优先的归结策略

Modus ponens、horn

前向链forward chaining

FC前向链的完备性证明

国科大高级人工智能8-归结原理和horn子句相关推荐

最新文章

热门文章