[工学]谓词逻辑.ppt

第四部分 数理逻辑 换名规则 代入规则 对象 约束变元 自由变元 范围 一个量词及其辖域内 整个公式 结果 只能换名为另一变元而 可以代入另一变元。 不能换名为个体常元， 还可代入个体常元， 换名后公式的含义不变。 公式由具有普遍意义变成 仅对该个体常元有意义。 定理10-2 任一谓词公式都可以化成为与之等值的前束范式。 证明 构造性算法步骤如下： 1. 消去联结词 ?，?。 2. 将联结词?向内深入，使之只作用于原子公式。 3. 利用换名或代入规则使所有约束变元的符号均不同，并且自由变元与约束变元的符号也不同。 4. 利用量词辖域的扩张和收缩律，将所有量词以在公式中出现的顺序移到公式最前面，扩大量词的辖域至整个公式。 例2 求公式 A：(?x P(x) ? ?y Q(y)) ? ?xR(x) 的前束范式。 解：A ? ?(?xP(x) ? ?yQ(y)) ? ?xR(x) 消去联结词 ? ? (??xP(x) ? ??yQ(y)) ? ?xR(x) 德 ? 摩根律 ? (?x?P(x) ? ?y?Q(y)) ? ?zR(z) 换名 ? ?x?y?z((?P(x) ? ?Q(y)) ? R(z)) 量词辖域扩张 例3 求公式 B：(?xP(x, y) ? ?yQ(y)) ? ?xR(x, y) 的前束范式。 解： B ? (?xP(x, t) ? ?yQ(y)) ? ?xR(x, t) 代入 ? (?xP(x, t) ? ?yQ(y)) ? ?zR(z, t) 换名 ? ?(??xP(x, t) ? ?yQ(y)) ? ?zR(z, t) 消去联结词 ? ? (?xP(x, t) ? ??yQ(y)) ? ?zR(z, t) ?向内深入 ? (?xP(x, t) ? ?y?Q(y)) ? ?zR(z, t) 量词转换 ? ?x(P(x, t) ? ?y?Q(y)) ? ?zR(z, t) 量词辖域扩张 ? ?x?y(P(x, t) ? ?Q(y)) ? ?zR(z, t) 量词辖域扩张 ? ?x?y?z(P(x, t) ? ?Q(y) ? R(z, t)) 量词辖域扩张 前束范式的优点在于它的量词全部集中在公式的前面，此部分称为公式的首标。 而公式的其余部分可看作是一个不含量词的谓词公式，它被称为公式的尾部。 在求给定谓词公式的前束范式时，对量词的左移的次序没有机械地规定，对于尾部也没有进一步的要求，因此一个公式的前束范式可以不唯一。 由于在谓词逻辑中的判定问题无解，因此前束范式并不象命题逻辑中的范式那样能解决判定问题。前束范式只是使公式的形式比较整齐规范，为判定工作提供一些方便。 定义10-12 设谓词公式 A 是一前束范式， 若 A 的尾部具有形式： 其中 Aij 是原子谓词公式或其否定，则称 A 是前束合取范式； 若 A 的尾部具有形式： 则称 A 是前束析取范式。 例5 将 A：?x(P(x) ? Q(x, y)) ? (??xR(x) ? ?zS(z)) 化为前束合取范式和前束析取范式。 解：(1) 消去联结词 ?，?： A ? ?x((P(x) ? Q(x, y)) ? (Q(x, y)?P(x))) ? (??xR(x) ? ?zS(z)) ? ??x((?P(x) ? Q(x, y)) ? (?Q(x, y) ? P(x))) ?(??xR(x) ? ?zS(z)) (2) 将联结词?深入至原子谓词公式： A ? ?x(?(?P(x) ? Q(x, y)) ? ?(?Q(x, y) ? P(x))) ? (?x?R(x) ? ?zS(z)) ? ?x(P(x) ? ?Q(x, y)) ? (Q(x, y) ? ?P(x))) ? (?x?R(x) ? ?zS(z)) (5) 利用分配律化其为前束合取范式： A ? ?x?t?z(((P(x) ? Q(x, y)) ? (?Q(x, y) ? ?P(x)) ? (?R(t)) ? S(z))) ? ?x?t?z(((P(x) ? (Q(x, y) ? ?R(t)) ? (?Q(x, y) ? ?P(x) ? S(z)) ? (?Q(x, y) ? ?P(x)) ? ?R(t)) ? (?Q(x, y) ? ?P(x)) ? S(z