第3章2消解原理.pptVIP

3.4 消 解 原 理 内容提要 置换、合一 子句集的求取 9个步骤 消解推理规则 含有变量的消解式 消解反演求解 谓词逻辑法（predicate logic） 谓词演算 1.语法与语义 2.连词和量词 谓词公式 1.定义 2.合适公式的性质 置换与合一 1.置换 2.合一算法 命题 def :具有真假意义的语句 命题的真值 命题逻辑有较大的局限性 无法描述客观事物的结构和逻辑特征 不能把不同事物间的共同特征表述出来 谓词 STUDENT ( tom ) GREATER( 5,3 ) 谓词公式的定义 原子谓词公式：用P(x1,x2,…,xn)表示一个n元谓词公式其中P为n元谓词，x1,x2,…xn为客体变量或变元。通常把P(x1,x2,…,xn)叫做谓词演算的原子公式，或原子谓词公式。 分子谓词公式：可以用连词把原子谓词公式组成复合谓词公式，并把它叫做分子谓词公式。 连词和量词 原子公式由若干谓词和个体组成,是谓词演算的基本块,用连词和量词将多个原子公式组合在一起,来表示复杂的含义. 用连词来连接若干个谓词组成一个谓词公式,用量词来刻划谓词和个体的关系 合取（conjunction）就是用连词∧把几个公式连接起来而构成的公式。合取项是合取式的每个组成部分。 蕴涵　 ? 表示如果-那么的语句。用连词?连接两个公式所构成的公式叫做蕴涵。 全称量词(Universal Quantifier)　若一个原子公式P(x)，对于所有可能变量x都具有T值，则用(? x)P(x)表示。 置换与合一 置换 形如{t1/x1,t2/x2,…,tn/xn}的有限集合。 其中，ti是项，xi是互不相同的变元；ti/xi表示用ti置换xi； 不允许ti与xi相同，也不允许变元xi循环地出现在另一个tj中。 合一 设有公式集F={F1,F2,…Fn},若存在一个置换s使得F1s=F2s=…=Fns，则称s是公式集F的一个合一，且称F1,F2,…Fn是可合一的。 置换举例 设有表达式P[x,f(y),B] ，对于置换： s1={z/x,w/y} s2={A/y} 分别有： P[x,f(y),B]s1= P[z,f(w),B] P[x,f(y),B]s2= P[x,f(A),B] 合一者、最一般合一者举例 设有表达式集{Ei}={P[x,f(y),B]，P[x,f(B),B]}， ①该表达式集的合一者：s1={B/y}，s2={w/x,B/y} ② s1={B/y}是该表达式集的最一般合一者。 （为什么？） 基本概念： 对谓词演算公式进行分解和化简，消去一些符号，以求得导出子句。 消解原理(resolution principle),也叫做归结原理。消解是一种可用于一定的子句公式的重要推理规则。 一子句定义为由文字的析取组成的公式(一个原子公式和原子公式的否定都叫做文字)。 当消解可使用时，消解过程被应用于母体子句对，以便产生一个导出子句。 eg，如果存在某个公理E1∨E2和另一公理～E2∨E3，那么E1∨E3在逻辑上成立。这就是消解，而称E1∨E3为E1∨E2和～E2∨E3的消解式(resolvent)。 子句集的求取 消去蕴涵符号 减少否定符号的辖域 对变量标准化 消去存在量词 skolem 函数 化为前束型 把母式化为合取范式 消去全称量词 消去连词符号? 更换变量名称 常用等价关系 常用等价关系 (1)消去蕴涵符号 只应用∨和～符号，以～A∨B替换A=B (3)对变量标准化 在任一量词辖域内，受该量词约束的变量为一哑元(虚构变量)，它可以在该辖域内处处统一地被另一个没有出现过的任意变量所代替，而不改变公式的真值。合适公式中变量的标准化，意味着对哑元改名以保证每个量词有其自己唯一的哑元。 (4)消去存在量词 Skolem函数: 在公式(? y)[(? x)P(x,y)]中，存在量词是在全称量词的辖域内，我们允许所存在的x可能依赖于y值。令这种依赖关系明显地由函数g(y)所定义，它把每个y值映射到存在的那个x。这种函数叫做Skolem函数。 如果用Skolem函数代替存在的x,我们就可以消去全部存在量词，并写成： (? y) P(g(y),y) Skolem函数所使用的函数符号必须是新的，即不允许是公式中已经出现过的函数符号。 从一个公式消去一个存在量词的一般规则是以一个Skolem函数代替每个出现的存在量词的量化变量，而这个Skolem函数的变量就是由那些全称量词所约束的全称量词量化变量，这些全称量词的辖域包括要被消去的存在量词的辖域在内。 如果要消去的存在量词不在任何一个全