中科院研究生院--人工智能原理课件.ppt

《中科院研究生院--人工智能原理课件.ppt》由会员上传分享，免费在线阅读，更多相关内容在教育资源-天天文库。

1、Agenda3.1引言3.2命题逻辑中的归结原理3.3谓词逻辑中的归结原理3.1Introduction证明的基本思想是：设F1、…、Fn、G为公式，G为F1、…、Fn的逻辑推论，当且仅当公式（（F1…Fn）G）是有效的也可以采用反证法的思想：设F1、…、Fn、G为公式，G为F1、…、Fn的逻辑推论，当且仅当公式（F1…FnG）是不可满足的归结法的本质上就是一种反证法，它是在归结推理规则的基础上实现的：为了证明一个命题P恒真，它证明其反命题～P恒假，即不存在使得P为真的解释3.2命题逻辑中的归结原理3.2.1子

2、句和子句形3.2.2归结3.2.3归结反演3.2.4合理性和完备性3.2.5归结反演的搜索策略3.2.1子句和子句形（1）文字是原子或其否定子句是文字的析取完备连接符集合：合取范式（CNF）（L11…L1n1)…(Lm1…Lmnm)析取范式（DNF）（L11…L1n1)…(Lm1…Lmnm)定理：对任意公式，都有与之等值的合取范式和析取范式转换方法：一般方法真值表方法3.2.2子句和子句形（2）一般方法Eliminateimplicationsignsbyusingtheequivalentformus

3、ingReducethescopesof~signsbyusingDeMorgan’slawandbyeliminatingdouble~signsConverttoCNFbyusingtheassociativeanddistributivelaws.3.2.2Resolution对任意三个子句p、q和rpr,q~rpq或者：forC1=PC1’,C2=~PC2’PC1’,~PC2’C1’C2’归结式：R(C1,C2)=C1’C2’证明：3.2.3ResolutionRefutations（1）定理证

4、明的任务:由前提A1A2...An推出结论B即证明:A1A2...AnB永真转化为证明:A1A2...An~B为永假式归结推理就是:从A1A2...An~B出发,使用归结推理规则来找出矛盾,最后证明定理A1A2...AnB的成立3.2.3ResolutionRefutations（2）归结方法是一种机械化的,可在计算机上加以实现的推理方法可认为是一种反向推理形式提供了一种自动定理证明的方法3.2.3ResolutionRefutations（3）一般过程:建立子句集S从子句集S出发,仅对S

5、的子句间使用归结推理规则如果得出空子句,则结束;否则转下一步将所得归结式仍放入S中对新的子句集使用归结推理规则转(3)空子句不含有文字,它不能被任何解释满足,所以空子句是永假的,不可满足的归结过程出现空子句,说明出现互补子句对,说明S中有矛盾,因此S是不可满足的.3.2.3ResolutionRefutations（4）例子:证明(PQ)~Q~p首先建立子句集:(PQ)~Q~(~P)(~PQ)~QPS={~PQ,~Q,P}对S作归结:(1)~PQ(2)~Q(3)P(4)~P(1)(2)归结(5)(3)(4

6、)归结3.2.4SoundnessandCompleteness归结原理是合理的归结原理是完备的3.2.5ResolutionRefutationSearchStrategies有序策略（Orderstrategies）Refinementstrategies支持集（Setofsupport）:每次归结时，参与归结的子句中至少应有一个是由目标公式的否定所得到的子句，或者是它们的后裔该策略是完备的线性输入（LinearInput）：参与归结的两个子句中至少有一个是初始子句集中的子句该策略是不完备的祖先过滤（AncestryFil

7、tering）：参与归结的两个子句中至少有一个是初始子句集中的句子，或者是另一个子句的祖先该策略是完备的