前束范式谓词推理.ppt

1 27 2020 discretemath 谓词公式的标准化形式 前束范式prenexnormalform PNF 前束合取范式前束析取范式 前束范式 1 27 2020 discretemath 在定理的机器证明中 需要消除谓词公式中的量词 因而需要将谓词公式中的量词前束化 即把公式中的量词均提取到公式的前部 即前束范式主要是对量词的位置有要求 而对联接词无要求 这一点与命题逻辑不同 前束范式作用 1 27 2020 discretemath 定义 一个谓词公式 如果它的所有量词均非否定地出现在公式的最前面 且它的辖域作用于整个公式 则称为此为前束范式 prenexnormalforms 即前束范式形如 Q1x1 Q2x2 Qkxk B其中Qi 1 i k 为 或 xi为客体变元 B为不含有量词的公式 前束范式 1 27 2020 discretemath 前束范式的特点是 所有量词均非否定地出现在公式最前面 且它的辖域一直延伸到公式之末 例如 x y z P x y Q y z R x y 是前束范式 而 xP x yQ y x P x yQ x y 不是前束范式 前束范式例子 1 27 2020 discretemath 前束范式存在定理 谓词逻辑中任意公式A都有与之等价的前束范式 转化方法 1 把条件或双条件联结词转化 2 利用量词否定等价公式 把否定深入到命题变元和谓词公式的前面 3 换名 4 利用量词作用域的扩张和收缩等价式 把量词提到前面 量词移前的步骤 1 27 2020 discretemath 前束范式例子 求下面公式的前束范式 1 xF x xG x 2 xF x xG x 1 27 2020 discretemath 求解前束范式例子 1 解 1 xF x xG x xF x yG y 换名规则 xF x y G y 量词否定 x F x y G y 辖域扩张 x y F x G y 辖域扩张 或者 xF x xG x xF x x G x 量词否定 x F x G x 量词分配 由此可知 1 中公式的前束范式是不唯一的 1 27 2020 discretemath 求解前束范式例子 2 2 xF x xG x xF x x G x 量词否定 xF x y G y 换名规则 x F x y G y 辖域扩张 x y F x G y 辖域扩张 问 2 的下述求法是否正确 xF x xG x xF x x G x x F x G x 错 1 27 2020 discretemath 1 27 2020 discretemath 例 求以下式的前束范式 1 xA x xB x 2 xA x xB x 3 x y z P x z P y z zQ x y z 解 1 xA x xB x x A x B x 即为所求前束范式 或 xA x xB x xA x xB x x A x xB x x A x B x 即为所求前束范式 前束范式例子 1 27 2020 discretemath 或 xA x xB x xA x yB y x A x yB y x y A x B y 即为所求前束范式 2 xA x xB x xA x yB y 换名 x A x yB y x y A x B y 前束范式例子 1 27 2020 discretemath 3 x y z P x z P y z zQ x y z x y z P x z P y z zQ x y z x y z P x z P y z zQ x y z x y z P x z P y z uQ 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 27 2020 discretemath 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 xB x 2 xA x xB x 3 x A x yB y A x 中无自由变元y 4 x A x yB x y A x 中无自由变元y 5 x y zA x y z zB x y z 前束范式练习 1 27 2020 discretemath 前束合取范式 定义 一个谓词公式A如果具有如下形式 则称为前束合取范式 Q1x1 Q2x2 Qnxn A11 A12 A1k1 A21 A22 A2k2 Am1 Am2 Amkm 其中Qi 1 i n 为 或 xi为客体变元 Aij是原子变元或其否定 1 27 2020 discretemath 前束析取范式 定义 一个谓词公式A如果具有如下形式 则称为前束析取范式 Q1x1 Q2x2 Qnxn A11 A12 A1k1 A21 A22 A2k2 Am1 Am2 Amkm 其中Qi 1 i n 为 或 xi为客体变元 Aij是原子变元或其否定 1 27 2020 discretemath 前束范式的的优点是全部量词集中在公式前面 其缺点是各量词的排列无一定规则 这样当把一个公式化归为前束范式时 其表达形式会不唯一 1920年斯柯林 Skolem 提出对前束范式首标中量词出现的次序给出规定 每个存在量词均在全称量词之前 按此规定得到的范式形式 称为斯柯林范式 显然 任一公式均可化为斯柯林范式 优点 全公式按顺序可分为三部分 公式的所有存在量词 所有全称量词和辖域 斯柯林范式 1 27 2020 discretemath 谓词逻辑的推理理论 谓词逻辑Lp是命题逻辑Ls的进一步深化和发展 因此Ls的推理理论在Lp中几乎可以完全照搬 在Lp中 某些前提和结论可能受到量词的约束 为确立前提和结论之间的内部联系 有必要消去量词和添加量词 正确理解和运用有关量词规则是Lp推理理论中的关键 1 27 2020 discretemath 谓词演算的推理理论 在谓词逻辑中 如果A1 A2 An B是逻辑有效式 则称B是A1 A2 An的有效结论 记作A1 A2 An BA B当且仅当A B是重言式例如 xF x xF x 1 27 2020 discretemath 全称指定规则US 或称为全称量词消去规则 xP x P c 这里P是谓词 而C是论域中某个任意的客体 另一种形式 xA x A y A x 对y是自由的 全称指定规则UIuniversalinstantiation 1 27 2020 discretemath 全称推广规则UG 全称量词产生规则 P x xP x 这个规则是要对命题量化 如果能够证明对论域中每一个客体C断言P c 成立 全称推广规则UGuniversalgeneralization 1 27 2020 discretemath 存在指定规则ES 或称为存在量词消去规则 xP x P c C是论域中的某些客体 必须注意 其指定的客体C不是任意的 存在指定规则EIexistentialinstantiation 1 27 2020 discretemath 存在推广规则EG 存在量词产生规则 P c xP x 这里C是论域中的一个客体 对于某些客体C成立 存在推广规则EGexistentialgeneralization 1 27 2020 discretemath 1 27 2020 discretemath 试证明下面的苏格拉底论证 所有人都是要死的 苏格拉底是人 因此 苏格拉底是要死的 证明 令M x x是人 D x x是要死的 s 苏格拉底 原题可符号化为 x M x D x M s D s 苏格拉底论证 1 27 2020 discretemath 推证如下 1 x M x D x 前提引入 2 M s D s UI 1 3 M s 前提引入 4 D s 2 3 假言推理 推证苏格拉底论证 1 27 2020 discretemath 谓词推理证明 x P x Q x x Q x R x x R x x P x 证明 x R x 前提引入 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 拒取式 x P x EG故 原推证成立 证毕 1 27 2020 discretemath 谓词推理例子 前提 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 1 27 2020 discretemath 谓词推理例子 证明 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是任意的 1 27 2020 discretemath 谓词推理例子 前提 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 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 1 27 2020 discretemath EXAMPLE1 Considerthefollowingstatements Thefirsttwoarecalledpremisesandthethirdiscalledtheconclusion Theentiresetiscalledanargument Alllionsarefierce凶猛的 Somelionsdonotdrinkcoffee Somefiercecreaturesdonotdrinkcoffee LetP x Q x andR x bethestatements xisalion xisfierce and xdrinkscoffee respectively Assumingthattheuniverseofdiscourseisthesetofallcreatures expressthestatementsintheargumentusingquantifiersandP x Q x andR x 1 27 2020 discretemath EXAMPLE2 Considerthefollowingstatements ofwhichthefirstthreearepremisesandthefourthisavalidconclusion Allhummingbirds蜂鸟arerichlycolored Nolargebirdsliveonhoney Birdsthatdonotliveonhoneyaredull晦暗的incolor Hummingbirdsaresmall LetP x Q x R x andS x bethestatements xisahummingbird xislarge xlivesonhoney and xisrichlycolored respectively Assumingthattheuniverseofdiscourseisthesetofallbirds expressthestatementsintheargumentusingquantifiersandP x Q x R x andS x 1 27 2020 discretemath 小结 1 前束范式2 推理理论 推理的形式结构 推理正确 构造证明 新的推理规则全称量词消去规则 记为UI全称量词引入规则 记为UG存在量词消去规则 记为EI存在量词引入规则 记为EG 1 27 2020 discretemath 学习要求 1 深刻理解重要的等值式 并能熟练地使用它们 2 熟练地使用置换规则 换名规则和代替规则 3 准确地求出给定公式的前束范式 形式可不唯一 4 正确地使用UI UG EI EG规则 特别地要注意它们之间的关系 5 对于给定的推理 正确地构造出它的证明 1 27 2020 discretemath 练习 P110 31 3 35 1 36 3 37 6 1 27 2020 discretemath 自然推理系统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 1 27 2020 discretemath 求解推理例子 1 1 前提 x F x G a R x xF x 结论 x F 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 1 27 2020 discretemath 求解推理例子 2 2 前提 x F x G x xG x 结论 xF x 证明 xG x 前提引入 x G x 置换 G c UI x F x G x 前提引入 F c G c UI F c 析取三段论 xF x EG 1 27 2020 discretemath 求解推理例子 3 3 前提 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 1 27 2020 discretemath 自然推理系统F推理例子 在自然推理系统F中 证明下面推理 1 每个有理数都是实数 有的有理数是整数 因此有的实数是整数 2 有理数 无理数都是实数 虚数不是实数 因此虚数既不是有理数 也不是无理数 3 不存在能表示成分数的无理数 有理数都能表示成分数 因此有理数都不是无理数 1 27 2020 discretemath 求解推理 1 设F x x为有理数 R x x为实数 G x x是整数 前提 x F x R x x F x G x 结论 x R x G x 证明 x F x G x 前提引入 F c G c EI F c 化简 G c 化简 x F x R x 前提引入 F c R c UI R c 假言推理 R c G c 合取 x R x G x EG 1 27 2020 discretemath 求解推理 2 设 F x x为有理数 G x x为无理数 R x 为实数 H x 为虚数前提 x F x G x R x x H x R x 结论 x H x F x G x 证明 x F x G x R x 前提引入 F y G y R y UI x H x R x 前提引入 H y R y UI R y F y G y 置换 H y F y G y 假言三段论 H y F y G y 置换 x H x F x G x UG 1 27 2020 discretemath 求解推理 3 设 F x x能表示成分数 G x x为无理数 H x 为有理数前提 x G x F x x H x F x 结论 x H x G x 证明 x H x F x 前提引入 H y F y UI x G x F x 前提引入 G y F y UI F y G y 置换 H y G y 假言三段论 x H x G x UG 1 27 2020 discretemath 讨论及提问 讨论及提问Anyquestion