Resolution 归结原理 | StriveZs的博客

Resolution 归结原理

Resolution 归结原理

和取范式

满足一种特殊形式的sentences,conjunction of disjunctions of literals(文字),一个原子命题的符号A或者他前面加上一个 都称为文字
disjunction of literals形式如:均用析取符号连接,比如
conjunction of disjunction of literals(和取范式): 多个disjunction of literals用合取符号连接
上面和的和取范式称为CNF。

语义等价 表示两个sentences可以互相转换(语义等价),比如, 可以参考knowledge 1中提供的语义等价公式表来进行转换。

figure.1

任何范式都是可以转换其他语义等价的合取范式。
将knowledge base中的任意一个sentence转换为一个CNF(通过语义等价),然后将合取去掉,分成一个个disjunction of literals,将分拆开的DOL(disjunction of literals简写)组成一个新的knowledge base。这样将一个原来的一个knowledge base转换为了一个新的 knowledge base(KB简写)。

归结

  • 找两个子句归结得到一个新的(可以分成很多种情况,类似一个树划分为无数个节点)
  • 然后进行继续划分节点搜索
  • 直到首次到达终止状态

Horn and Definite Clauses

  • 正文字,负文字(带否符号的)
  • Defineite clauses: 很多个文字的析取,而且这些文字中有且仅有一个是正的
  • Horn Clauses: 很多文字的析取,至多有一个正的,也可以全是负的
  • 两个Horn Clauses进行归结得到的Clauses一定是一个Hron Clauses
  • 析取为disjunction,合取为conjunction
StriveZs wechat
Hobby lead  creation, technology change world.