版权说明:本文档由用户提供并上传,收益归属内容提供方,若内容存在侵权,请进行举报或认领
文档简介
1、1 主要内容主要内容 l 一阶逻辑等值式与基本的等值式一阶逻辑等值式与基本的等值式 l 置换规则、换名规则、代替规则置换规则、换名规则、代替规则 l 前束范式前束范式 l 自然推理系统自然推理系统NL 及其推理规则及其推理规则 第五章第五章 一阶逻辑等值演算与推理一阶逻辑等值演算与推理 2 5.1 一阶逻辑等值式与置换规则一阶逻辑等值式与置换规则 定义定义5.1 设设A, B是两个谓词公式是两个谓词公式, 如果如果AB是永真式是永真式, 则称则称A 与与B等值等值, 记作记作AB, 并称并称AB是是等值式等值式 基本等值式基本等值式 第一组第一组 命题逻辑中命题逻辑中16组基本等值式的代换实例
2、组基本等值式的代换实例 例如,例如,xF(x)xF(x), xF(x)yG(y) xF(x)yG(y) 等等 第二组第二组 (1) 消去量词等值式消去量词等值式 设设D =a1, a2, , an xA(x) A(a1) A(a2) A(an) xA(x) A(a1) A(a2) A(an) 3 基本等值式基本等值式 (2) 量词否定等值式量词否定等值式 xA(x) x A(x) xA(x) x A(x) (3) 量词辖域收缩与扩张等值式量词辖域收缩与扩张等值式. A(x) 是含是含 x 自由出现的公式,自由出现的公式,B 中不含中不含 x 的自由出现的自由出现 关于全称量词的:关于全称量词的
3、: x(A(x) B) xA(x) B x(A(x) B) xA(x) B x(A(x)B) xA(x)B x(BA(x) BxA(x) 4 基本等值式基本等值式 关于存在量词的:关于存在量词的: x(A(x) B) xA(x) B x(A(x) B) xA(x) B x(A(x)B) xA(x)B x(BA(x) BxA(x) (4) 量词分配等值式量词分配等值式 x(A(x) B(x) xA(x)xB(x) x(A(x) B(x) xA(x)xB(x) 注意:注意: 对对 , 对对 无分配律无分配律 5 置换规则、换名规则、代替规则置换规则、换名规则、代替规则 1. 置换规则置换规则 设设
4、 (A)是含是含A的公式的公式, 那么那么, 若若AB, 则则 (A) (B). 2. 换名规则换名规则 设设A为一公式,将为一公式,将A中某量词辖域中个体变项的所有约束中某量词辖域中个体变项的所有约束 出现及相应的指导变元换成该量词辖域中未曾出现过的个出现及相应的指导变元换成该量词辖域中未曾出现过的个 体变项符号,其余部分不变,设所得公式为体变项符号,其余部分不变,设所得公式为A ,则,则AA. 3. 代替规则代替规则 设设A为一公式,将为一公式,将A中某个个体变项的所有自由出现用中某个个体变项的所有自由出现用A中中 未曾出现过的个体变项符号代替,其余部分不变,设所得未曾出现过的个体变项符号
5、代替,其余部分不变,设所得 公式为公式为A ,则,则AA. 6 实例实例 例例1 将下面命题用两种形式符号化将下面命题用两种形式符号化, 并证明两者等值并证明两者等值: (1) 没有不犯错误的人没有不犯错误的人 解解 令令F(x):x是人,是人,G(x):x犯错误犯错误. x(F(x)G(x) 或或 x(F(x)G(x) x(F(x)G(x) x (F(x) G(x) 量词否定等值式量词否定等值式 x( F(x) G(x) 置换置换 x(F(x)G(x) 置换置换 7 实例实例 (2) 不是所有的人都爱看电影不是所有的人都爱看电影 解解 令令F(x):x是人,是人,G(x):爱看电影:爱看电影
6、. x(F(x)G(x) 或或 x(F(x)G(x) x(F(x)G(x) x (F(x)G(x) 量词否定等值式量词否定等值式 x ( F(x) G(x) 置换置换 x(F(x)G(x) 置换置换 8 实例实例 例例2 将公式化成等值的不含既有约束出现、又有自由出现将公式化成等值的不含既有约束出现、又有自由出现 的个体变项的个体变项: x(F(x,y,z)yG(x,y,z) 解解 x(F(x,y,z)yG(x,y,z) x(F(x,y,z)tG(x,t,z) 换名规则换名规则 x t(F(x,y,z)G(x,t,z) 辖域扩张等值式辖域扩张等值式 或者或者 x(F(x,y,z)yG(x,y,
7、z) x(F(x,u,z)yG(x,y,z) 代替规则代替规则 x y(F(x,u,z)G(x,y,z) 辖域扩张等值式辖域扩张等值式 9 实例实例 例例3 设个体域设个体域D=a,b,c, 消去下述公式中的量词消去下述公式中的量词: (1) x y(F(x)G(y) 解解 x y(F(x)G(y) ( y(F(a)G(y) ( y(F(b)G(y) ( y(F(c)G(y) (F(a)G(a) (F(a)G(b) (F(a)G(c) (F(b)G(a) (F(b)G(b) (F(b)G(c) (F(c)G(a) (F(c)G(b) (F(c)G(c) 10 实例实例 解法二解法二 x y(F
8、(x)G(y) x(F(x)yG(y) 辖域缩小等值式辖域缩小等值式 x(F(x)G(a) G(b) G(c) (F(a)G(a) G(b) G(c) (F(b)G(a) G(b) G(c) (F(c)G(a) G(b) G(c) 11 实例实例 (2) x yF(x,y) x yF(x,y) x(F(x,a) F(x,b) F(x,c) (F(a,a) F(a,b) F(a,c) (F(b,a) F(b,b) F(b,c) (F(c,a) F(c,b) F(c,c) 12 5.2 一阶逻辑前束范式一阶逻辑前束范式 定义定义5.2 设设A为一个一阶逻辑公式,若为一个一阶逻辑公式,若A具有如下形
9、式具有如下形式 Q1x1Q2x2QkxkB 则称则称A为为前束范式前束范式,其中,其中Qi (1 i k)为为 或或 ,B为不含量词为不含量词 的公式的公式. 例如,例如, x (F(x) G(x) x y(F(x)(G(y) H(x,y) 是前束范式是前束范式 而而 x(F(x) G(x) x(F(x)y(G(y) H(x,y) 不是前束范式,不是前束范式, 13 前束范式存在定理前束范式存在定理 定理定理5.1(前束范式存在定理)(前束范式存在定理) 一阶逻辑中的任何公式都存在与之等值的前束范式一阶逻辑中的任何公式都存在与之等值的前束范式 例例4 求下列公式的前束范式求下列公式的前束范式
10、(1) x(M(x) F(x) 解解 x(M(x) F(x) x( M(x)F(x) (量词否定等值式)(量词否定等值式) x(M(x)F(x) 后两步结果都是前束范式,说明公式的前束范式不惟一后两步结果都是前束范式,说明公式的前束范式不惟一. 14 求前束范式的实例求前束范式的实例 (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
11、(x)G(y) 辖域收缩扩张规则辖域收缩扩张规则 15 求前束范式的实例求前束范式的实例 (3) xF(x)y(G(x,y)H(y) 或或 xF(x)y(G(z,y)H(y) 代替规则代替规则 x y(F(x)(G(z,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) 辖域收缩扩张规则辖域收缩扩张规则 16 5.3 一阶逻辑的推论理论一阶逻辑的推论理论 推理的形式结构推理的形式结构 1. A1 A2Ak B 若次式是永真式若次式是永真式, 则称推理正确则称推理正确, 记作记作A1 A2Ak B
12、2. 前提前提: A1, A2, Ak 结论结论: B 推理定理推理定理: 永真式的蕴涵式永真式的蕴涵式 17 推理定理推理定理 第一组第一组 命题逻辑推理定理的代换实例命题逻辑推理定理的代换实例 如如, xF(x)yG(y) xF(x) 第二组第二组 基本等值式生成的推理定理基本等值式生成的推理定理 如如, xF(x) xF(x), xF(x) xF(x) xF(x)x F(x), x F(x) xF(x) 第三组第三组 其他常用推理定律其他常用推理定律 (1) xA(x)xB(x) x(A(x) B(x) (2) x(A(x) B(x)xA(x)xB(x) (3) x(A(x)B(x) x
13、A(x)xB(x) (4) x(A(x)B(x) xA(x)xB(x) 18 量词消去引入规则量词消去引入规则 1. 全称量词消去规则全称量词消去规则( -) 或或 其中其中x,y是个体变项符号是个体变项符号, c是个体常项符号是个体常项符号, 且在且在A中中x不在不在 y 和和 y的辖域内自由出现的辖域内自由出现. 2. 全称量词引入规则全称量词引入规则( +) 其中其中x是个体变项符号是个体变项符号, 且不在前提的任何公式中自由出现且不在前提的任何公式中自由出现 xA(x) A(y) xA(x) A(c) A(x) xA(x) 19 量词消去引入规则量词消去引入规则 3. 存在量词消去规则
14、存在量词消去规则( -) 其中其中x是个体变项符号是个体变项符号, 且不在前提的任何公式和且不在前提的任何公式和B中自由中自由 出现出现 A(x)B xA(x)B 20 量词消去引入规则量词消去引入规则 4. 存在量词引入消去规则存在量词引入消去规则( +) 或或 或或 其中其中x,y是个体变项符号是个体变项符号, c是个体常项符号是个体常项符号, 且在且在A中中y和和c不在不在 x和和 x的辖域内自由出现的辖域内自由出现. BA(y) BxA(x) BA(c) BxA(x) A(y) xA(x) A(c) xA(x) 21 自然推理系统自然推理系统NL 定义定义5.3 自然推理系统自然推理系
15、统NL 定义如下定义如下: 1. 字母表字母表. 同一阶语言同一阶语言L 的字母表的字母表 2. 合式公式合式公式. 同同L 的合式公式的合式公式 3. 推理规则推理规则: (1) 前提引入规则前提引入规则 (2) 结论引入规则结论引入规则 (3) 置换规则置换规则 (4) 假言推理规则假言推理规则 (5) 附加规则附加规则 (6) 化简规则化简规则 (7) 拒取式规则拒取式规则 22 自然推理系统自然推理系统NL (8) 假言三段论规则假言三段论规则 (9) 析取三段论规则析取三段论规则 (10) 构造性二难推理规则构造性二难推理规则 (11) 合取引入规则合取引入规则 (12) -规则规则
16、 (13) +规则规则 (14) -规则规则 (15) +规则规则 推理的证明推理的证明 23 构造推理证明的实例构造推理证明的实例 例例5 在自然推理系统在自然推理系统NL 中构造下面推理的证明中构造下面推理的证明, 取个体域取个体域R: 任何自然数都是整数任何自然数都是整数. 存在自然数存在自然数. 所以所以, 存在整数存在整数. 解解 设设F(x):x是自然数是自然数, G(x):x是整数是整数. 前提前提: x(F(x)G(x), xF(x) 结论结论: xG(x) 证明证明: x(F(x)G(x) 前提引入前提引入 F(x)G(x) - F(x)xG(x) + xF(x)xG(x)
17、- xF(x) 前提引入前提引入 xG(x) 假言推理假言推理 24 构造推理证明的实例构造推理证明的实例 例例6 在自然推理系统在自然推理系统NL 中构造下面推理的证明中构造下面推理的证明, 取个体域取个体域R: 不存在能表示成分数的无理数不存在能表示成分数的无理数. 有理数都能表示成分数有理数都能表示成分数. 所以所以, 有理数都不是无理数有理数都不是无理数. 解解 设设F(x):x是无理数是无理数, G(x):x是有理数是有理数, H(x):x能表示成分数能表示成分数. 前提前提: x(F(x) H(x), x(G(x)H(x) 结论结论: x(G(x)F(x) 证明证明: x(F(x)
18、 H(x) 前提引入前提引入 x( F(x)H(x) 置换置换 x(F(x)H(x) 置换置换 F(x)H(x) - 25 构造推理证明的实例构造推理证明的实例 x(G(x)H(x) 前提引入前提引入 G(x)H(x) - H(x)F(x) 置换置换 G(x)F(x) 假言三段论假言三段论 x(G(x)F(x) + 26 重要提示重要提示 yxyxF :),( 要特别注意使用要特别注意使用 -、 +、 -、 +规则的条件规则的条件. 反例反例1. 对对A= x yF(x,y)使用使用 -规则规则, 推得推得B= yF(y,y). 取解释取解释I: 个体域为个体域为R, 在在I下下A被解释为被解
19、释为 x y(xy), 真真; 而而B被解释为被解释为 y(yy), 假假 原因原因: 在在A中中x自由出现自由出现在在 y的辖域的辖域F(x,y)内内 反例反例2. 前提前提: P(x)Q(x), P(x) 结论结论: xQ(x) 取解释取解释I: 个体域为个体域为Z, 在在I下前提为下前提为真真, 结论为假结论为假, 从而推理不正确从而推理不正确 整除整除被被是偶数是偶数2:)(,:)(xxQxxP 27 反例反例2(续续) “证明证明”: P(x)Q(x) 前提引入前提引入 P(x) 前提引入前提引入 Q(x) 假言推理假言推理 xQ(x) + 错误原因错误原因: 在在使用使用 +规则规
20、则, 而而x在前提的公式中自由出现在前提的公式中自由出现. 28 第五章第五章 习题课习题课 主要内容主要内容 l 一阶逻辑等值式一阶逻辑等值式 基本等值式,置换规则、换名规则、代替规则基本等值式,置换规则、换名规则、代替规则 l 前束范式前束范式 l 推理的形式结构推理的形式结构 l 自然推理系统自然推理系统NL 推理定律、推理规则推理定律、推理规则 29 基本要求基本要求 l 深刻理解并牢记一阶逻辑中的重要等值式深刻理解并牢记一阶逻辑中的重要等值式, 并能准确而熟并能准确而熟 练地应用它们练地应用它们 l 熟练正确地使用置换规则、换名规则、代替规则熟练正确地使用置换规则、换名规则、代替规则
21、 l 熟练地求出给定公式的前束范式熟练地求出给定公式的前束范式 l 深刻理解自然推理系统深刻理解自然推理系统NL 的定义,牢记的定义,牢记NL 中的各条推理中的各条推理 规则,特别是注意使用规则,特别是注意使用、 +、 +、 4条推理规则的条推理规则的 条件条件 l 能正确地给出有效推理的证明能正确地给出有效推理的证明 30 练习练习1 2 a 1. 给定解释给定解释I如下如下: (1) 个体域个体域D=2,3 (2) (3) (4) 求下述在求下述在I下的解释及其真值下的解释及其真值: x y(F(f(x) G(y,f(a) 2)3(, 3)2(:)( ffxf 0)3 , 3(, 1)2
22、, 3()3 , 2()2 , 2(:),( 1)3(, 0)2(:)( GGGGyxG FFxF 解解 xF(f(x)yG(y,f(a) F(f(2) F(f(3) (G(2,f(2) G(3,f(2) 1 0 (1 0)0 31 练习练习2 2.求下述公式的前束范式求下述公式的前束范式: xF(x)y(G(x,y) H(x,y) 解解 使用换名规则使用换名规则, xF(x)y(G(x,y) H(x,y) zF(z)y(G(x,y) H(x,y) z(F(z)y(G(x,y) H(x,y) z y(F(z)(G(x,y) H(x,y) 使用代替规则使用代替规则 xF(x)y(G(x,y) H
23、(x,y) xF(x)y(G(z,y) H(z,y) x(F(x)y(G(z,y) H(z,y) x y(F(x)(G(z,y) H(z,y) 32 练习练习3 3.构造下面推理的证明构造下面推理的证明: (1) 前提:前提: x(F(x)G(x), xF(x) 结论:结论: xG(x) 证明:证明: x(F(x)G(x) 前提引入前提引入 F(y)G(y) xF(x) 前提引入前提引入 F(y) G(y) 假言推理假言推理 yG(y) + xG(x) 置换置换 33 练习练习3(续续) (2) 前提:前提: x(F(x) G(x), xG(x) 结论:结论: xF(x) 证明:用归谬法证明:用归谬法 xF(x) 结论否定引入结论否定引入 x F(x) 置换置换 xG(x) 前提引入前提引入 x G(x) 置换置换 x(F(x) G(x), 前提引入前提引入 F(c) G(c) F(c) G(c) G(c) 析取三段论析取三段论 G(c) G(
温馨提示
- 1. 本站所有资源如无特殊说明,都需要本地电脑安装OFFICE2007和PDF阅读器。图纸软件为CAD,CAXA,PROE,UG,SolidWorks等.压缩文件请下载最新的WinRAR软件解压。
- 2. 本站的文档不包含任何第三方提供的附件图纸等,如果需要附件,请联系上传者。文件的所有权益归上传用户所有。
- 3. 本站RAR压缩包中若带图纸,网页内容里面会有图纸预览,若没有图纸预览就没有图纸。
- 4. 未经权益所有人同意不得将文件中的内容挪作商业或盈利用途。
- 5. 人人文库网仅提供信息存储空间,仅对用户上传内容的表现方式做保护处理,对用户上传分享的文档内容本身不做任何修改或编辑,并不能对任何下载内容负责。
- 6. 下载文件中如有侵权或不适当内容,请与我们联系,我们立即纠正。
- 7. 本站不保证下载资源的准确性、安全性和完整性, 同时也不承担用户因使用这些下载资源对自己和他人造成任何形式的伤害或损失。
最新文档
- 医院医辅工作制度
- 医院控烟工作制度
- 医院社工工作制度
- 华西团委工作制度
- 协会监事工作制度
- 单位信创工作制度
- 咖啡店长工作制度
- 急救站抢救工作制度
- 总务处巡检工作制度
- 情绪发泄室工作制度
- 国家广播电视总局部级社科研究项目申请书
- 2025-2030中国自行车行业市场深度调研及发展趋势与投资前景预测研究报告
- 2026年陕西延长石油集团有限责任公司校园招聘笔试备考题库及答案解析
- 工会2025年度工作报告国企2025工会工作报告
- 广东梅州市嘉城建设集团有限公司招聘笔试题库2026
- T∕SZSSIA 019-2026 反恐怖防范管理规范 总则
- 2026年及未来5年市场数据中国税务大数据行业市场全景分析及投资前景展望报告
- 2026年中考英语专题复习:5个主题作文 预测练习题(含答案+范文)
- 2026年陕西能源职业技术学院单招职业适应性考试题库附参考答案详解(完整版)
- 24J113-1 内隔墙-轻质条板(一)
- 神州数码人才测评题2
评论
0/150
提交评论