前束范式谓词推理.ppt

1、8/5/2020,discrete math,谓词公式的标准化形式： 前束范式prenex normal form(PNF) 前束合取范式 前束析取范式,前束范式,8/5/2020,discrete math,在定理的机器证明中，需要消除谓词公式中的量词，因而需要将谓词公式中的量词前束化，即把公式中的量词均提取到公式的前部。即前束范式主要是对量词的位置有要求，而对联接词无要求，这一点与命题逻辑不同。,前束范式作用,8/5/2020,discrete math,定义： 一个谓词公式，如果它的所有量词均非否定地出现在公式的最前面，且它的辖域作用于整个公式，则称为此为前束范式（prenex norm

2、al forms）。即前束范式形如 (Q1x1)(Q2x2)(Qkxk)B 其中Qi(1ik)为或， xi为客体变元。B为不含有量词的公式。,前束范式,8/5/2020,discrete math,前束范式的特点是，所有量词均非否定地出现在公式最前面，且它的辖域一直延伸到公式之末。 例如，xyz(P(x,y)Q(y,z) R(x,y) 是前束范式。 而xP(x)yQ(y)，x(P(x)yQ(x,y) 不是前束范式。,前束范式例子,8/5/2020,discrete math,前束范式存在定理： ：谓词逻辑中任意公式A都有与之等价的前束范式。 转化方法： 1、把条件或双条件联结词转化。 2、利用

3、量词否定等价公式，把否定深入到命题变元和谓词公式的前面。 3、换名。 4、利用量词作用域的扩张和收缩等价式，把量词提到前面。,量词移前的步骤,8/5/2020,discrete math,前束范式例子,求下面公式的前束范式： (1)xF(x)xG(x) (2) xF(x)xG(x),8/5/2020,discrete math,求解前束范式例子(1),解 (1)xF(x)xG(x) xF(x)yG(y) (换名规则) xF(x)yG(y) (量词否定) x(F(x) yG(y) (辖域扩张) xy(F(x)G(y) (辖域扩张) 或者 xF(x)xG(x) xF(x)xG(x) (量词否定)

4、x(F(x)G(x) (量词分配) 由此可知，(1)中公式的前束范式是不唯一的。,8/5/2020,discrete math,求解前束范式例子(2),(2) xF(x)xG(x) xF(x)xG(x) (量词否定) xF(x)yG(y) (换名规则) x(F(x)yG(y) (辖域扩张) xy(F(x)G(y) (辖域扩张) 问：(2)的下述求法是否正确？ xF(x)xG(x) xF(x) xG(x) x(F(x)G(x) 错,8/5/2020,discrete math,8/5/2020,discrete math,例：求以下式的前束范式： （1）xA(x)x B(x) （2）xA(x)x

5、 B(x) （3）xy (z(P(x,z)P(y,z)z Q(x,y,z),解（1）xA(x)x B(x) x(A(x)B (x) 即为所求前束范式。 或xA(x)x B(x) xA(x)x B(x) xA(x)x B(x) x(A(x)B(x) 即为所求前束范式。,前束范式例子,8/5/2020,discrete math,或xA(x)x B(x) xA(x)y B(y) x(A(x)y B(y) xy (A(x)B(y) 即为所求前束范式。 (2)xA(x)x B(x) xA(x)yB(y) (换名) x(A(x)yB(y) xy (A(x)B(y),前束范式例子,8/5/2020,dis

6、crete math,(3) xy (z(P(x,z)P(y,z)z Q(x,y,z) xy (z(P(x,z)P(y,z)z Q(x,y,z) xy(z(P(x,z)P(y,z)z Q(x,y,z) xy (z(P(x,z)P(y,z)u Q(x,y,u) xy zu (P(x,z)P(y,z)Q(x,y,u) （或xy zu (P(x,z)P(y,z)Q(x,y,u)）,前束范式例子,8/5/2020,discrete math,1、设个体域D=d1, ,dn，试用消去量词的方式证明：当A(x)中无自由变元y ，B(y) 中无自由变元x时， x y (A(x)B(y) yx (A(x)B(

7、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）xy (zA(x,y,z) z B(x,y,z),前束范式练习,8/5/2020,discrete math,前束合取范式,定义：一个谓词公式A如果具有如下形式，则称为前束合取范式： (Q1x1)(Q2x2)(Qnxn)(A11A12A1k1)(A21A22A2k2)(Am1Am2Amkm) 其中Qi (1in）为或，xi为客体变元，Aij是原子变元或其否定。,8/5/

8、2020,discrete math,前束析取范式,定义：一个谓词公式A如果具有如下形式，则称为前束析取范式： (Q1x1)(Q2x2)(Qnxn)(A11A12A1k1)(A21A22A2k2)(Am1Am2Amkm) 其中Qi (1in）为或，xi为客体变元，Aij是原子变元或其否定。,8/5/2020,discrete math,前束范式的的优点是全部量词集中在公式前面，其缺点是各量词的排列无一定规则，这样当把一个公式化归为前束范式时，其表达形式会不唯一。 1920年斯柯林(Skolem)提出对前束范式首标中量词出现的次序给出规定：每个存在量词均在全称量词之前。按此规定得到的范式形式，称

9、为斯柯林范式。 显然，任一公式均可化为斯柯林范式。 优点：全公式按顺序可分为三部分，公式的所有存在量词、所有全称量词和辖域。,斯柯林范式,8/5/2020,discrete math,谓词逻辑的推理理论,谓词逻辑Lp是命题逻辑Ls的进一步深化和发展，因此Ls的推理理论在Lp中几乎可以完全照搬。 在Lp中，某些前提和结论可能受到量词的约束，为确立前提和结论之间的内部联系，有必要消去量词和添加量词。 正确理解和运用有关量词规则是Lp推理理论中的关键。,8/5/2020,discrete math,谓词演算的推理理论,在谓词逻辑中，如果A1A2AnB是逻辑有效式，则称B是A1, A2, ，An的有效

10、结论，记作 A1A2AnB AB 当且仅当 AB是重言式 例如： xF(x) xF(x),8/5/2020,discrete math,全称指定规则US，或称为全称量词消去规则, xP (x) P (c) 这里P是谓词，而C是论域中某个任意的客体。 另一种形式：xA(x)A(y) A(x)对y是自由的,全称指定规则UI universal instantiation,8/5/2020,discrete math,全称推广规则UG，全称量词产生规则,P (x) x P (x) 这个规则是要对命题量化，如果能够证明对论域中每一个客体C断言P(c)成立。,全称推广规则UG universal gen

11、eralization,8/5/2020,discrete math,存在指定规则ES，或称为存在量词消去规则, xP (x) P (c) C是论域中的某些客体，必须注意，其指定的客体C不是任意的。,存在指定规则EI existential instantiation,8/5/2020,discrete math,存在推广规则EG，存在量词产生规则,P (c) x P (x) 这里C是论域中的一个客体，对于某些客体C成立。,存在推广规则EG existential generalization,8/5/2020,discrete math,8/5/2020,discrete math,试证明下

12、面的苏格拉底论证： 所有人都是要死的， 苏格拉底是人， 因此，苏格拉底是要死的。 证明： 令M(x):x是人，D(x):x是要死的，s:苏格拉底，原题可符号化为： x(M(x)D(x)，M(s) D(s),苏格拉底论证,8/5/2020,discrete math,推证如下： （1） x(M(x)D(x) 前提引入 （2） M(s)D(s) UI（1） （3） M(s) 前提引入 （4） D(s) (2)(3)假言推理,推证苏格拉底论证,8/5/2020,discrete math,谓词推理证明,x(P(x)Q(x)，x(Q(x)R(x)，xR(x) xP(x) 证明： xR(x) 前提引入

13、R(c) EI x(Q(x)R(x) 前提引入 Q(c)R(c) UI Q(c) 析取三段论 x(P(x)Q(x) 前提引入 P(c)Q(c) UI P(c) 拒取式 xP(x) EG 故，原推证成立，证毕。,8/5/2020,discrete math,谓词推理例子,前提: x(F(x)G(x)，xF(x) 结论: xG(x) 证明: (1) xF(x) 前提引入 (2) F(c) EI (1) (3) x(F(x)G(x) 前提引入 (4) F(c)G(c) UI(3) (5) G(c) (2)(4)假言推理 (6) xG(x) EG(5) 注意证明过程为：“先EI，后UI”,8/5/20

14、20,discrete math,谓词推理例子,证明: (1) x(F(x)G(x) 前提引入 (2) F(c)G(c) UI (2) (3) xF(x) 前提引入 (4) F(c) EI (3) 注意：这个证明是错的. (3)(4)应当在(1)(2)之前， (4)中的c是特定的， (2)中的c是任意的。,8/5/2020,discrete math,谓词推理例子,前提: x(F(x)H(x), x(G(x)H(x), 结论: x(G(x)F(x) 证明: (1) x(F(x)H(x) 前提引入 (2) x(F(x)H(x) (1) 量词否定 (3) x(H(x)F(x) (2) 靡根律 (4

15、) H(y)F(y) UI(3) (5) x(G(x)H(x) 前提引入 (6) G(y)H(y) UI(5) (7) G(y)F(y) (4)(6) 假言三段论 (8) x(G(x)F(x) UG(7),8/5/2020,discrete math,EXAMPLE 1,Consider the following statements. The first two are called premises and the third is called the conclusion. The entire set is called an argument. All lions are fie

16、rce凶猛的 . Some lions do not drink coffee. Some fierce creatures do not drink coffee. Let P(x), Q(x), and R(x) be the statements x is a lion, x is fierce, and x drinks coffee, respectively. Assuming that the universe of discourse is the set of all creatures, express the statements in the argument usin

17、g quantifiers and P(x), Q(x), and R(x).,8/5/2020,discrete math,EXAMPLE 2,Consider the following statements, of which the first three are premises and the fourth is a valid conclusion. All hummingbirds蜂鸟are richly colored. No large birds live on honey. Birds that do not live on honey are dull晦暗的 in c

18、olor. Hummingbirds are small. Let P(x), Q(x), R(x), and S(x) be the statements x is a hummingbird, x is large, x lives on honey, and x is richly colored, respectively. Assuming that the universe of discourse is the set of all birds, express the statements in the argument using quantifiers and P(x),

19、Q(x), R(x), and S(x).,8/5/2020,discrete math,小结,1、前束范式 2、推理理论推理的形式结构推理正确构造证明新的推理规则 全称量词消去规则，记为UI 全称量词引入规则，记为UG 存在量词消去规则，记为EI 存在量词引入规则，记为EG,8/5/2020,discrete math,学习要求,1、深刻理解重要的等值式，并能熟练地使用它们。 2、熟练地使用置换规则、换名规则和代替规则。 3、准确地求出给定公式的前束范式（形式可不唯一）。 4、正确地使用UI、UG、EI、EG规则，特别地要注意它们之间的关系。 5、对于给定的推理，正确地构造出它的证明。,8/

20、5/2020,discrete math,练 习,P110 ： 31(3)、35(1)、36(3)、37(6),8/5/2020,discrete math,自然推理系统F推理例子,在自然推理系统F中构造下面推理的证明：(1) 前提：x(F(x)(G(a)R(x)，xF(x)结论： x(F(x)R(x)(2) 前提：x(F(x)G(x)，xG(x)结论： xF(x)(3) 前提： x(F(x)G(x)， x(G(x)R(x)， xR(x)结论： xF(x),8/5/2020,discrete math,求解推理例子(1),(1) 前提：x(F(x)(G(a)R(x)，xF(x)结论： x(F(

21、x)R(x)证明: xF(x) 前提引入 F(c) EI x(F(x)(G(a)(R(x) 前提引入 F(c)(G(a)R(c) UI G(a)R(c) 假言推理 R(c) 化简 F(c)R(c) 合取 x(F(x)R(x) EG,8/5/2020,discrete math,求解推理例子(2),(2) 前提：x(F(x)G(x)，xG(x)结论： xF(x) 证明： xG(x) 前提引入 xG(x) 置换 G(c) UI x(F(x)G(x) 前提引入 F(c)G(c) UI F(c) 析取三段论 xF(x) EG,8/5/2020,discrete math,求解推理例子(3),(3) 前

22、提： x(F(x)G(x)， x(G(x)R(x)， xR(x)结论： xF(x)证明： x(F(x)G(x) 前提引入 F(y)G(y) UI x(G(x)R(x) 前提引入 G(y)R(y) UI xR(x) 前提引入 R(y) UI G(y) 析取三段论 F(y) 析取三段论 xF(x) UG,8/5/2020,discrete math,自然推理系统F推理例子,在自然推理系统F中，证明下面推理：(1) 每个有理数都是实数，有的有理数是整数，因此有的实数是整数。(2) 有理数、无理数都是实数，虚数不是实数，因此虚数既不是有理数、也不是无理数。(3) 不存在能表示成分数的无理数，有理数都能表示成分数，因此有理数都不是无理数。,8/5/202