离散数学)谓词逻辑.ppt

前束范式 定义2-3.３:如果在前束范式（Q1x1）（Q2x2）…（Qnxn）G中,母式G是合取(或析取)范式,相应地称这个前束范式为前束合取(或析取)范式。 定理2-3.6 每一个含量词的谓词公式都存在着与之等价的前束范式。 化规过程: 1.将公式中?,?化成～ ,?,? 2.利用量词转换律Ｅ25,Ｅ26和德.摩根定律,将否定直接移到原子公式前。 3.利用约束变元的改名和自由变元的代入规则,使所有约束变元之间,自由变元与约束变元之间均不同名。 4. 利用量词的扩张与收缩,把量词移到全式的最前面。 * * 前束范式 例2.4 将公式(?xP(x)∨?yR(y))??xF(x) 化规为前束范式。 解：(?xP(x)∨?yR(y))??xF(x) ? ～(?xP(x)∨?yR(y))∨?xF(x) (1) ? (?x～P(x)∧?y～R(y))∨?xF(x) (2) ? （?x～P(x)∧?y～R(y)）∨ ?z F(z) (3) ? ?x?y?z( (～P(x)∧～R(y) )∨F(z) ) (4) (析取范式) ? ?x?y?z((～P(x)∨F(z))∧(～R(y) ∨ F(z)) (合取范式) * * 前束范式的不足 把一个谓词公式变成等价的前束范式时,可能存在多个全称量词和存在量词. 凡是同一类型的量词,可以交换顺序而不影响等价性； 全称量词和存在量词一般不能交换顺序； 两种量词出现的顺序可能组成多种情况； 在处理实际问题时很不方便。人们设计了一种解决办法： 只保留全称量词,而把存在量词转化为相应的依赖函数,这就是Skolem范式的思路。 * * 斯柯林(Skolem)范式 斯柯林(Skolem)范式----不含存在量词的前束合取范式 定义2－3.4 设谓词公式A的等价前束合取范式是 （Q1x1）（Q2x2）…（Qnxn）G, １）从左到右扫描量词，设Qi是第一个遇到的存在量词: ①如i=1,则选择一个在G中未使用过的常量标识符代替G中的全部x1,然后删去Q1x1; ②如果i1,则Q1,Q2,…Qi-1都是全称量词,这时选择一个在G中未使用过的函数标识符(如g)，并用g(x1,x2,..,xi-1)去代替G中的全部xi,然后删去Qixi; 2）重复这一过程,直到公式中不含存在量词为止。 这样得到的公式称为Skolem范式,而取代存在量词时使用的常量标识符或函数,称为Skolem函数。 * * 斯柯林(Skolem)范式 例2.5 求?x?y?z?u?v?wP(x,y,z,u,v,w)的Skolem范式。 解： ?x?y?z?u?v?wP(x,y,z,u,v,w) ?y?z?u?v?wP(a,y,z,u,v,w)（消去?x） ?y?z?v?w P(a,y,z,f(y,z),v,w) （消去?ｕ） ?y?z?vP(a,y,z,f(y,z),v,g(y,z,v)) （消去?ｗ） * * Skolem范式的理解 消去存在量词,将相应变元以函数代入的理解: 如 ?x?yP(x,y)的Skolem范式是?xP(x,f(x)) ∵ ?x?yP(x,y)的意思是对任一x都有一个y使P(x,y)成立, 这个y通常是依赖x的,可视为x的某个函数f(x),从而有Skolem范式?xP(x,f(x)) 。 然而能找到的y不一定是x的函数f, 于是?x?yP(x,y)与?xP(x,f(x))并不等值。 如Ｄ={1,2}, ?x?yP(x,y)?(P(1,1)∨P(1,2))∧(P(2,1)∨P(2,2)) 与?xP(x,f(x)) ?P(1,f(1))∧P(2,f(2)) 两者明显不等值,但在不可满足的意义下是一致的。 * * 斯柯林(Skolem)范式 　定理2－3.7 设谓词公式G的Skolem范式为S,则G为矛盾式当且仅当 S为矛盾式。 Skolem范式是一种重要的范式形式，机器定理证明和逻辑程序设计中的消解(或称归结)原理就建立在这种范式的基础上。 * * 作业 习题二 5（1）、（3） 6（2） 7（2）、（3） 8 9 10 11（1）、（2） * * Chapter 2 一阶谓词逻辑(2) Chapter 1 命题逻辑 Company Logo Company Logo Company Logo 栾新成 四川大学软件学院 luanxch@第2章 一阶谓词逻辑(2) 主要内容 谓词公式与解释 1.谓词的合适公式 2.谓词公式的解释