谓词演算的推理理论-永真推理系统.ppt

第四章谓词演算的推理理论 4 1谓词演算的永真推理系统4 1 1公理系统的组成部分4 1 2公里系统的推理过程4 2谓词演算的假设推理系统4 3谓词演算的归结推理系统 4 1 1公理系统的组成部分 一 语法部分 一 基本符号 二 公理 三 规则二 语义部分三 关于公理的几点说明 一 基本符号 公理系统所允许出现的全体符号的集合 1 命题变元 P Q R 等字母表示命题变元 2 个体变元 x y 等小写字母表示个体变元 3 谓词变元 X Y 等大写字母表示谓词变元 4 联结词 是联结词 5 量词 全称量词 存在量词 6 括号 是括号 7 全称封闭符 基本符号 续 8 合式公式 i 原子命题P是合式公式 ii 谓词填式A x1 x2 x3 xn 是合式公式 iii 若A是公式 则 A是合式公式 iv 若A和B是合式公式 则 A B A B A B A B 为公式 v 若A是合式公式 x是A中出现的任何个体变元 则 xA x xA x 为合式公式 vi 只有有限次使用 i ii iii iv v 所得到的式子才是合式公式 基本符号 续 9 全称封闭式 设 为含有n个自由变元的公式 如果在 前用全称量词把n个自由变元约束起来后所得到的公式 称为 的全称封闭式 记为 例写出下式的全称封闭式 xP x y uQ u v 解 xP x y uQ u v y v xP x y uQ u v 二 公理 公理1 P P 公理2 P Q R Q P R 公理3 P Q Q R P R 公理4 P P Q P Q 公理5 P Q P Q 公理6 P Q Q P 公理7 P Q Q P P Q 调头 传递 凝缩 二 公理 公理8 P Q P 公理9 P Q Q 公理10 P Q P Q 公理11 P P Q 公理12 Q P Q 公理13 P R Q R P Q R 公理14 P Q Q P 公理15 P P 二 公理 公理20 xP x P x 公理21 P x xP x 如果只有一个自由变元 公理20与公理21可以分别理解如下 x yP y P x x P x yP y 三 规则 1 分离规则 如果 A B 且 A 则 B 2 全称规则 P x xP x 其中 中不含自由的x 3 全称量词消去规则 xP x P x x可以为任意的变元 4 存在量词引入规则 P x xP x 其中 中不含自由的x 回顾 量词作用域的收缩与扩张 设公式 中不含有自由的x 则下面的公式成立 x x x x x x x x x x x x x x x x 存在量词引入 全称量词引入 二 语义部分 1 公理是永真公式 2 规则规定如何从永真公式推出永真公式 分离规则指明 如果 A B 永真且 A永真 则 B也为永真公式 3 定理为永真公式 它们是从公理出发利用上述规则推出来的公式 三 关于公理的几点说明 1 本系统中不引入代入规则 它的作用由下面的 2 来实现 2 本系统中的所有公理我们把它看作公理模式 即只要形如某一公理 我们就称其为某一公理 如 P P P Q R P Q R xP x xP x 等均为公理1 第四章谓词演算的推理理论 4 1谓词演算的永真推理系统4 1 1公理系统的组成部分4 1 2公里系统的推理过程4 2谓词演算的假设推理系统4 3谓词演算的归结推理系统 例1 p41 已知定理 P Q P 求证 全0规则 x x x 证明 1 x 2 x P P x 引用定理 3 P P x 2 1 分离 4 P P x x 全称规则 3 5 P P 公理 1 6 x x 4 5 分离则有全0规则 x x x 全n规则 存n规则 全n规则 1 2 n x 1 2 n x x 存n规则 1 2 n x 1 2 n x x 全1规则 全称规则 存0规则 存在规则 例试利用存0规则求证存1规则 1 x 1 x x 证明 1 1 x 2 1 x x 1 公理2 3 x 1 分离 1 2 4 x x 1 存0规则 5 x x 1 1 x x 公理2 6 1 x x 分离 5 6 两次运用调头公理2 例 练习4 1 1 x P x xP x 证明 x P x P x 公理20 P x 与P x 同形 2 x P x xP x 全2规则 1 2 x 1 2 x x 例 续 x P x xP x 再证明 xP x x P x 证明 3 xP x P x 公理20 4 xP x P x xP x P x 定理 5 xP x P x 分离 3 4 6 xP x x P x 全1规则 定理 P Q R P R Q 例 再续 x P x xP x 已经证得 2 6 两式 2 x P x xP x 6 xP x x P x 于是 7 x P x xP x xP x x P x x P x xP x 公理7 8 xP x x P x x P x xP x 分离 2 7 9 x P x xP x 分离 6 8 例 练习4 1 2 x P x xP x 先证明 x P x xP x 证明 1 x P x P x 公理20 2 x P x xP x 存1规则 1 P x 1 xP x 例 续 x P x xP x 再证明 xP x x P x 证明 3 P x xP x 公理21 4 P x xP x xP x P x 公理3 5 xP x P x 分 3 4 6 xP x x P x 全称规则 例 再续 x P x xP x 已经证得 2 6 两式 2 x P x xP x 6 xP x x P x 于是有 7 x P x xP x xP x x P x x P x xP x 公理7 8 xP x x P x x P x xP x 分离 2 7 9 x P x xP x 分离 6 8 例 练习4 2 已知公理 A P Q P B P P 及分离规则和全称规则 全称规则为 1 2 x 1 2 x x 试证 全0规则 x x x 证 1 x 2 P Q P 公理A 3 x P P x 代入 1 4 P P x 1 3 分离 5 P P x P P P P x 代入 2 6 P P P P x 4 5 分离 7 P P P P x x 全称规则 8 P P 公理B 9 P P x x 7 8 分离 10 x x 9 8 分离 例2 p42 试证明 A x P x xP x 证 A 1 x P x P x 公理20 x P x P x P x x P x 公理14 3 P x x P x 2 1 分离 4 xP x x P x 存在量词引入规则 3 xP x x P x x P x xP x 公理14 6 x P x xP x 5 4 分离 例2 p42 已知定理 P Q Q P 试证明 B xP x x P x 证 B 7 P x xP x 公理21 8 P x xP x xP x P x 已知定理 9 xP x P x 8 7 分离 10 xP x x P x 全称规则 9 例2 p42 试证明 x P x xP x 证明 已经分别证出如下 6 10 两式 x P x xP x 10 xP x x P x 11 x P x xP x xP x x P x x P x xP x 公理7 12 xP x x P x x P x xP x 11 6 分离 13 x P x xP x 12 10 分离 例4 p43 P Q x P xQ x 证明 1 Q x xQ x 公理21 2 P Q x Q x xQ x P xQ x 公理3 3 P Q x Q x xQ x P x