3.2前束范式谓词推理课件.pptVIP

谓词公式的标准化形式： 前束范式prenex normal form(PNF) 前束合取范式 前束析取范式;在定理的机器证明中，需要消除谓词公式中的量词，因而需要将谓词公式中的量词前束化，即把公式中的量词均提取到公式的前部。即前束范式主要是对量词的位置有要求，而对联接词无要求，这一点与命题逻辑不同。;定义： 一个谓词公式，如果它的所有量词均非否定地出现在公式的最前面，且它的辖域作用于整个公式，则称为此为前束范式（prenex normal forms）。即前束范式形如 (Q1x1)(Q2x2)…(Qkxk)B 其中Qi(1≤i≤k)为?或?， xi为客体变元。B为不含有量词的公式。;前束范式的特点是，所有量词均非否定地出现在公式最前面，且它的辖域一直延伸到公式之末。 例如，?x?y?z((P(x,y)?Q(y,z)) ? R(x,y)) 是前束范式。 而?xP(x)??yQ(y)，?x(P(x)??yQ(x,y)) 不是前束范式。;前束范式存在定理： ：谓词逻辑中任意公式A都有与之等价的前束范式。 转化方法： 1、把条件或双条件联结词转化。 2、利用量词否定等价公式，把否定深入到命题变元和谓词公式的前面。 3、换名。 4、利用量词作用域的扩张和收缩等价式，把量词提到前面。;前束范式例子;求解前束范式例子(1);求解前束范式例子(2);;例：求以下式的前束范式： （1）?xA(x)→?x B(x) （2）?xA(x)∨?x B(x) （3）?x?y (?z(P(x,z)∧P(y,z))→?z Q(x,y,z));或?xA(x)→?x B(x) ??xA(x)→?y B(y) ??x(A(x)→?y B(y)) ??x?y (A(x)→B(y)) 即为所求前束范式。 (2)?xA(x)∨?x B(x) ??xA(x)∨?yB(y) (换名) ??x(A(x)∨?yB(y)) ??x?y (A(x)∨B(y));(3) ?x?y (?z(P(x,z)∧P(y,z))→?z Q(x,y,z)) ??x?y (┐?z(P(x,z)∧P(y,z))∨?z Q(x,y,z)) ??x?y(?z(┐P(x,z)∨┐P(y,z))∨?z Q(x,y,z)) ??x?y (?z(┐P(x,z)∨┐P(y,z))∨?u Q(x,y,u)) ??x?y ?z?u (┐P(x,z)∨┐P(y,z)∨Q(x,y,u)) （或??x?y ?z?u (P(x,z)∧P(y,z)→Q(x,y,u))）; 1、设个体域D=?d1, …,dn?，试用消去量词的方式证明：当A(x)中无自由变元y ，B(y) 中无自由变元x时， ?x ?y (A(x)∧B(y)) ? ?y?x (A(x)∧B(y)) 2、求下列各式的前束范式： （1）?xA(x)→?x B(x) （2）?xA(x)∧?x B(x) （3）┐?x (A(x)→?y B(y)) (A(x)中无自由变元y) （4）?x (A(x)→?y B(x,y)) (A(x)中无自由变元y) （5）?x?y (?zA(x,y,z) ??z B(x,y,z));前束合取范式;前束析取范式;前束范式的的优点是全部量词集中在公式前面，其缺点是各量词的排列无一定规则，这样当把一个公式化归为前束范式时，其表达形式会不唯一。 1920年斯柯林(Skolem)提出对前束范式首标中量词出现的次序给出规定：每个存在量词均在全称量词之前。按此规定得到的范式形式，称为斯柯林范式。 显然，任一公式均可化为斯柯林范式。 优点：全公式按顺序可分为三部分，公式的所有存在量词、所有全称量词和辖域。;谓词逻辑的推理理论;谓词演算的推理理论;全称指定规则US，或称为全称量词消去规则;全称推广规则UG，全称量词产生规则;存在指定规则ES，或称为存在量词消去规则;存在推广规则EG，存在量词产生规则;;试证明下面的苏格拉底论证： 所有人都是要死的， 苏格拉底是人， 因此，苏格拉底是要死的。 证明： 令M(x):x是人，D(x):x是要死的，s:苏格拉底，原题可符号化为： ?x(M(x)?D(x))，M(s) ? D(s);推证如下： （1） ?x(M(x)?D(x)) 前提引入 （2） M(s)?D(s) UI（1） （3） M(s) 前提引入 （4） D(s) (2)(3)假言推理;谓词推理证明;谓词推理例子;谓