人工智能(2)侯宏旭 cshhximu.edu.cn归结推理 可以在计算机上实现的推理方法 Herbrand命题逻辑的归结法 证明A1A2 A3B为真 等价于证明A1A2 A3 B为假 反演推理 步骤 建立子句集 对子句集进行归结 C1=PC1，C2=PC2 =R(C1,C2)=C1 C2 归结到空子句表明出现了矛盾，即得证谓词逻辑的推理 转换为子句形 SKOLEM标准形 转换为前束范式 转换成合取范式 消去量词 从左至右 存在量词变成左边所有全称量词的函数 SKOLEM标准型和原公式不等价G和S的不可满足性 G：原公式 S：对应的SKOLEM标准型 G不可满足当且仅当S不可满足H域 对G，定义在D上，令H0是G中出现的常量集 合，如果G中没有常量，任取a 另Hi=Hi-1T，其中T是Hi-1中运算通过所有函 数运算后得到的集合 H就是G的H域H解释 由子句集和H域可以衍生出所有的文字集A 对A中的命题指派真假值就可以形成所有的 H解释 S不可满足，当且仅当S在H域上不可满足， 即对所有H解释都为假语义树 由命题构造语义树 按文字取值真假形成二叉树的分支 谓词逻辑中的语义树 生成H集 在H集上建立文字集 可能生成无限语义树利用语义树证明 遍历语义树既是给出所有解释 若所有叶子节点（其对应的解释）取假， 则语义树不可满足 如果遍历到某个节点即取假，则其后继节 点不需要继续遍历，这个节点称为失败节 点 如果所有分支上都存在失败节点，则语义 树是一个封闭树Herbrand定理 S不可满足当且仅当其对应的语义树是一个 封闭树 S不可满足，当且仅当存在不可满足的有限 基例集删除规则 删除重言式 单文字删除 L，LC1，L C2，C3，C4可以简化为 C2,C3,C4 纯文字删除 只出现L,而不出现L 删除蕴含式 L， LC1 分离规则