离散数学 2.3 一阶逻辑等值式.ppt

1 2 3一阶逻辑等值式 等值式基本等值式量词否定等值式量词辖域收缩与扩张等值式量词分配等值式前束范式 2 等值式与基本等值式 基本等值式 命题逻辑中16组基本等值式的代换实例如 xF x xF x xF x xF x yG y xF x yG y xF x yG y xF x yG y 定义设A B是一阶逻辑中的任意两个公式 若A B为逻辑有效式 则称A与B是等值的 记作A B 并称A B为等值式 3 基本等值式 消去量词等值式设D a1 a2 an 1 xA x A a1 A a2 A an 2 xA x A a1 A a2 A an 量词否定等值式 1 xA x x A x 2 xA x x A x 4 基本等值式 续 量词辖域收缩与扩张等值式设A x 是含x自由出现的公式 B中不含x的出现关于全称量词的 x A x B xA x B x A x B xA x B x A x B xA x B x B A x B xA x 关于存在量词的 x A x B xA x B x A x B xA x B x A x B xA x B x B A x B xA x 5 基本的等值式 续 量词分配等值式 x A x B x xA x xB x x A x B x xA x xB x 注意 对 无分配律 对 无分配律 量词等值式 x yA x y y xA x y x y y xA x y 其中A x y 是x y自由出现的谓词公式 6 基本的等值式 续 例将下面命题用两种形式符号化 1 没有不犯错误的人 2 不是所有的人都爱看电影解 1 令F x x是人 G x x犯错误 x F x G x x F x G x 请给出演算过程 并说明理由 2 令F x x是人 G x 爱看电影 x F x G x x F x G x 给出演算过程 并说明理由 7 前束范式 例如 x y F x G y H x y x F x G x 是前束范式 而 x F x y G y H x y x F x G x 不是前束范式 定义设A为一个一阶逻辑公式 若A具有如下形式Q1x1Q2x2 QkxkB 则称A为前束范式 其中Qi 1 i k 为 或 B为不含量词的公式 8 公式的前束范式 定理 前束范式存在定理 一阶逻辑中的任何公式都存在与之等值的前束范式注意 公式的前束范式不惟一求公式的前束范式的方法 利用重要等值式 置换规则 换名规则 代替规则进行等值演算 9 换名规则与代替规则 换名规则 将量词辖域中出现的某个约束出现的个体变项及对应的指导变项 改成另一个辖域中未曾出现过的个体变项符号 公式中其余部分不变 则所得公式与原来的公式等值 代替规则 对某自由出现的个体变项用与原公式中所有个体变项符号不同的符号去代替 则所得公式与原来的公式等值 10 公式的前束范式 续 例求下列公式的前束范式 1 x M x F x 解 x M x F x x M x F x 量词否定等值式 x M x F x 两步结果都是前束范式 说明前束范式不惟一 11 例 续 2 xF x xG x 解 xF x xG x xF x x G x 量词否定等值式 x F x G x 量词分配等值式 另有一种形式 xF x xG x xF x x G x xF x y G y 代替规则 x y F x G y 量词辖域扩张 两种形式是等值的 12 例 续 3 xF x xG x 解 xF x xG x xF x x G x x F x G x 为什么 或 x y F x G y 为什么 4 xF x y G x y H y 解 xF x y G x y H y zF z y G x y H y 换名规则 z y F z G x y H y 为什么 13 例 续 或 xF x y G z y H y 代替规则 x y F x G z y H y 5 x F x y y G x y H x z 解用换名规则 也可用代替规则 这里用代替规则 x F x y y G x y H x z x F x u y G x y H x z x y F x u G x y H x z 注意 x与 y不能颠倒 14 2 4一阶逻辑推理理论 推理的形式结构判断推理是否正确的方法重要的推理定律推理规则构造证明附加前提证明法 15 推理 推理的形式结构有两种 第一种A1 A2 Ak B 第二种前提 A1 A2 Ak结论 B其中A1 A2 Ak B为一阶逻辑公式 若 为永真式 则称推理正确 否则称推理不正确 判断方法 真值表法 等值演算法 主析取范式法及构造证明法 前3种方法采用第一种形式结构 构造证明法采用第二种形式结构 16 重要的推理定律 第一组命题逻辑推理定律代换实例如 xF x yG y xF x 为化简律代换实例 第二组由基本等值式生成如由 xA x x A x 生成 xA x x A x x A x xA x 第三组 xA x xB x x A x B x x A x B x xA x xB x x A x B x xA x xB x x A x B x xA x xB x 17 推理规则 1 前提引入规则 2 结论引入规则 3 置换规则 4 假言推理规则 5 附加规则 6 化简规则 7 拒取式规则 8 假言三段论规则 9 析取三段论规则 10 构造性二难推理规则 11 合取引入规则 18 推理规则 续 12 全称量词消去规则 简记为UI规则或UI 两式成立的条件是 x是A x 中的自由出现的个体变项在第一式中 取代x的y应为任意的不在A x 中约束出现的个体变项 在第二式中 c为任意个体常项 用y或c去取代A x 中的自由出现的x时 一定要在x自由出现的一切地方进行取代 19 推理规则 续 13 全称量词引入规则 简记为UG规则或UG 该式成立的条件是 y是A y 中自由出现的个体变项 无论y取何值 A y 应该均为真 取代自由出现的y的x 也不能在A y 中约束出现 20 推理规则 续 14 存在量词引入规则 简记为EG规则或EG 该式成立的条件是 c是使A为真的特定个体常项 取代c的x不能在A c 中出现过 21 推理规则 续 15 存在量词消去规则 简记为EI规则或EI 该式成立的条件是 c是使A为真的特定的个体常项 c不在A x 中出现 若A x 中除自由出现的x外 还有其他自由出现的个体变项 此规则不能使用 22 构造推理证明 例1证明苏格拉底三段论 人都是要死的 苏格拉底是人 所以苏格拉底是要死的 令F x x是人 G x x是要死的 a 苏格拉底前提 x F x G x F a 结论 G a 证明 F a 前提引入 x F x G x 前提引入 F a G a UI G a 假言推理注意 使用UI时 用a取代x 23 构造推理证明 续 例2乌鸦都不是白色的 北京鸭是白色的 因此 北京鸭不是乌鸦 令F x x是乌鸦 G x x是北京鸭 H x x是白色的前提 x F x H x x G x H x 结论 x G x F x 24 例2 续 证明 x F x H x 前提引入 F y H y UI x G x H x 前提引入 G y H y UI H y G y 置换 F y G y 假言三段论 G y F y 置换 x G x F x UG 25 构造推理证明 续 例3构造下述推理证明前提 x F x G x xF x 结论 xG x 证明 xF x 前提引入 x F x G x 前提引入 F c EI F c G c UI G c 假言推理 xG x EG注意 必须先消存在量词 26 构造推理证明 续 例4构造下述推理证明前提 xF x xG x 结论 x F x G x 证明 xF x xG x 前提引入 x y F x G y 置换 x F x G z UI F z G z UI x F x G x