人工智能原理第4章消解法

《人工智能原理第4章消解法》由会员上传分享，免费在线阅读，更多相关内容在教育资源-天天文库。

1、人工智能原理第4章消解法本章内容4.1消解法的基本思想4.2Herbrand定理4.3消解法4.4消解策略参考书目第4章消解法4.1消解法的基本思想第4章消解法消解法的基本思想从第3章逻辑系统中可知，逻辑推理必须考虑其有效性(即∑

2、=A)，即对论域中的任何赋值都能保证公式为真由可靠性定理知：逻辑系统中任何正确的推理，都要具有“如果∑

3、—A则∑

4、=A”的性质，即证明推理的有效性从有效性和可满足性的关系可知，有效性等价于其否命题的不可满足性第4章消解法4消解法基本思想:反证法这样就引出了消解法，其基本思想就是反证法即：要证命题(理解为经典逻辑的公式)A恒为

5、真，等价于证﹁A恒为假从语义上解释，恒为假就是不存在一个论域上的一个赋值(可称为解释)，使﹁A为真，即对所有的论域上的所有赋值，﹁A均为假但是，论域本身和解释有无穷多个，不可能一一验证第4章消解法5基本思想(1)Herbrand提出：从所有解释当中选出一种有代表性的解释，并严格证明一旦命题在代表性解释中为假，则在所有解释中为假Herbrand定义了这样的论域和代表性解释，称为Herbrand论域(H论域)和Herbrand解释(H解释)有定理—公式A(无前束范式)是不可满足的，当且仅当A在所有Herbrand赋值下都取假值第4章消解法6基本思想(2)

6、这样，在证假(不可满足)的意义上使公式与子句集的语义解释等价、并与H解释等价，作为消解法的开端但如何找到H解释？引入语义树，让所有解释都展现在语义树上最后在改进寻找解释算法的复杂性中发现了消解式，从而构成了消解法的完整理论基础消解也叫归结，本章混用这两个称呼第4章消解法74.2Herbrand定理4.2.1公式到子句集的转换4.2.2Herbrand论域和解释4.2.3语义树4.2.4Herbrand定理4.2.5不可满足基子句集第4章消解法证明的步骤证明一个公式A在给定论域下恒为真，也就是要证明﹁A恒为假将﹁A转化为一个子句集，集合中元素为原子公式或

7、其析取/通过其中正负原子公式的合并(此时恒为真，对证假不起作用，因此消去)/最后集合为空，说明是不可满足的，即恒为假通常形式：证明﹁(A→B)为假即A∧﹁B为假，也即对应子句集归结为空子句首先介绍基本术语复习和公式到子句集的转换第4章消解法94.2.1公式到子句集的转换首先复习几个定义：文字(literal)：正原子公式和负原子公式称为文字，同一原子公式的正和负称为互补的。子句(clause)：文字的析取称为子句。合取范式：形如A1∧A2∧…∧An的公式，其中A1～An均为子句。前束范式：形如(Q1x1…Qnxn)M(x1…xn)的公式，M中不再含有量

8、词。Skolem标准形：在前束范式中消去存在量词后得到的公式第4章消解法10消去存在量词消去存在量词的步骤：(1)若存在量词不在任何全称量词之后，则公式中被存在量词量化的变量以某个不同于公式中任何其他常量名字的常量c代替，并消去存在量词；(2)若存在量词在k个全称量词之后，则公式中被存在量词量化的变量用被前k个全称量词量化的变量x1～xk的某个函数f(x1～xk)的形式代替，f的名字不同于公式中任何其他函数的名字，但对函数形式没有要求；然后消去存在量词/函数f称为Skolem函数第4章消解法11公式转化为子句集的步骤(1)公式A化为子句集S，其实现步骤

9、共9步，如下：(1)消去等价和蕴含符号：蕴含转化为析取(2)将否定符号转移到每个谓词之前：应用狄摩根定律(3)变量标准化：约束变量各不相同(4)消去存在量词：存在量词不受全称量词约束，则变量用常量替换/如果存在量词受全称量词约束，则使用Skolem函数替换相应变量——得到Skolem标准形第4章消解法12公式转化为子句集的步骤(2)(5)公式化为前束型：全部全称量词移到公式的最前面/得到的两部分称为前缀和母式(6)母式化为合取范式：外层连接符全部是合取，里层连接符全部为析取(7)去掉所有全称量词(8)母式化为子句集：每个合取项间的合取符号(∧)用逗号代

10、替，即得子句集(9)子句变量标准化：每个子句中的变量各不相同第4章消解法13公式与子句集的等价实现消解法的基础是把参与推理的每个公式都转化为子句集/通过逐步对消子句集合中互补的文字(即L和﹁L)而最终得到一个空子句□，证明原来的公式是不可满足的反证法定理：给定公式A及相应的子句集S，则A是不可满足的当且仅当S是不可满足的使用子句集进行消解法推理，其过程是完备的—即如果公式X是子句集S的逻辑推论，则X可以从S中推出第4章消解法144.2.2Herbrand论域和解释Herbrand论域定义Herbrand论域(H论域)：设S为子句集，H0是S中子句所含的

11、全体常量集，若S中子句不含常量，则任选一常量a令H0={a}。对i≥1令Hi=Hi-1∪{f(