人工智能原理课件

ThePrinciplesofAI-----WangWenjieResolution:1©GraduateSchool,ChineseacademyofSciences.Spring2004•來自www.3722.cn中国最大的资料库下载Agenda3.1引言3.2命题逻辑中的归结原理3.3谓词逻辑中的归结原理ThePrinciplesofAI-----WangWenjieResolution:2©GraduateSchool,ChineseacademyofSciences.Spring2004•來自www.3722.cn中国最大的资料库下载3.1Introduction•证明的基本思想是：设F1、…、Fn、G为公式，G为F1、…、Fn的逻辑推论，当且仅当公式（（F1…Fn）G）是有效的•也可以采用反证法的思想：设F1、…、Fn、G为公式，G为F1、…、Fn的逻辑推论，当且仅当公式（F1…FnG）是不可满足的•归结法的本质上就是一种反证法，它是在归结推理规则的基础上实现的：为了证明一个命题P恒真，它证明其反命题～P恒假，即不存在使得P为真的解释ThePrinciplesofAI-----WangWenjieResolution:3©GraduateSchool,ChineseacademyofSciences.Spring2004•來自www.3722.cn中国最大的资料库下载3.2命题逻辑中的归结原理3.2.1子句和子句形3.2.2归结3.2.3归结反演3.2.4合理性和完备性3.2.5归结反演的搜索策略ThePrinciplesofAI-----WangWenjieResolution:4©GraduateSchool,ChineseacademyofSciences.Spring2004•來自www.3722.cn中国最大的资料库下载3.2.1子句和子句形（1）•文字是原子或其否定•子句是文字的析取•完备连接符集合：•合取范式（CNF）（L11…L1n1)…(Lm1…Lmnm)•析取范式（DNF）（L11…L1n1)…(Lm1…Lmnm)•定理：对任意公式，都有与之等值的合取范式和析取范式•转换方法：一般方法真值表方法ThePrinciplesofAI-----WangWenjieResolution:5©GraduateSchool,ChineseacademyofSciences.Spring2004•來自www.3722.cn中国最大的资料库下载3.2.2子句和子句形（2）•一般方法–Eliminateimplicationsignsbyusingtheequivalentformusing–Reducethescopesof~signsbyusingDeMorgan’slawandbyeliminatingdouble~signs–ConverttoCNFbyusingtheassociativeanddistributivelaws.ThePrinciplesofAI-----WangWenjieResolution:6©GraduateSchool,ChineseacademyofSciences.Spring2004•來自www.3722.cn中国最大的资料库下载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’•证明：ThePrinciplesofAI-----WangWenjieResolution:7©GraduateSchool,ChineseacademyofSciences.Spring2004•來自www.3722.cn中国最大的资料库下载3.2.3ResolutionRefutations（1）•定理证明的任务:由前提A1A2...An推出结论B即证明:A1A2...AnB永真•转化为证明:A1A2...An~B为永假式•归结推理就是:从A1A2...An~B出发,使用归结推理规则来找出矛盾,最后证明定理A1A2...AnB的成立來自www.3722.cn中国最大的资料库下载ThePrinciplesofAI-----WangWenjieResolution:8©GraduateSchool,ChineseacademyofSciences.Spring2004•來自www.3722.cn中国最大的资料库下载3.2.3ResolutionRefutations（2）•归结方法是一种机械化的,可在计算机上加以实现的推理方法•可认为是一种反向推理形式•提供了一种自动定理证明的方法ThePrinciplesofAI-----WangWenjieResolution:9©GraduateSchool,ChineseacademyofSciences.Spring2004•來自www.3722.cn中国最大的资料库下载3.2.3ResolutionRefutations（3）•一般过程:1)建立子句集S2)从子句集S出发,仅对S的子句间使用归结推理规则3)如果得出空子句,则结束;否则转下一步4)将所得归结式仍放入S中5)对新的子句集使用归结推理规则6)转(3)•空子句不含有文字,它不能被任何解释满足,所以空子句是永假的,不可满足的•归结过程出现空子句,说明出现互补子句对,说明S中有矛盾,因此S是不可满足的.ThePrinciplesofAI-----WangWenjieResolution:10©GraduateSchool,ChineseacademyofSciences.Spring2004•來自www.3722.cn中国最大的资料库下载3.2.3ResolutionRefutations（4）•例子:证明(PQ)~Q~p•首先建立子句集:–(PQ)~Q~(~P)–(~PQ)~QP–S={~PQ,~Q,P}•对S作归结:(1)~PQ(2)~Q(3)P(4)~P(1)(2)归结(5)(3)(4)归结ThePrinciplesofAI-----WangWenjieResolution:11©GraduateSchool,ChineseacademyofSciences.Spring2004•來自www.3722.cn中国最大的资料库下载3.2.4SoundnessandCompleteness•归结原理是合理的•归结原理是完备的ThePrinciplesofAI-----WangWenjieResolution:12©GraduateSchool,ChineseacademyofSciences.Spring2004•來自www.3722.cn中国最大的资料库下载3.2.5ResolutionRefutationSearchStrategies•有序策略（Orderstrategies）•Refinementstrategies1.支持集（Setofsupport）:每次归结时，参与归结的子句中至少应有一个是由目标公式的否定所得到的子句，或者是它们的后裔该策略是完备的2.线性输入（LinearInput）：参与归结的两个子句中至少有一个是初始子句集中的子句该策略是不完备的3.祖先过滤（AncestryFiltering）：参与归结的两个子句中至少有一个是初始子句集中的句子，或者是另一个子句的祖先该策略是完备的