《第五章 一阶逻辑等值演算与推理》由会员分享，可在线阅读，更多相关《第五章 一阶逻辑等值演算与推理（39页珍藏版）》请在金锄头文库上搜索。
1、2019/10/17,1,主要内容 一阶逻辑等值式与基本的等值式 置换规则、换名规则、代替规则 前束范式 自然推理系统NL 及其推理规则,第五章 一阶逻辑等值演算与推理,2019/10/17,2,5.1 一阶逻辑等值式与置换规则,在一阶逻辑中,有些命题可以有不同的符号形式,如命题 “没有不犯错误的人”取全总个体域时有两种不同的符号 形式:,令F(x)：x是人，G(x)：x犯错误. (1) x(F(x)G(x) (2) x(F(x)G(x),同命题逻辑的情况一样,称(1)与(2)是等值的.,2019/10/17,3,5.1 一阶逻辑等值式与置换规则,定义5.1 设A, B是两个谓词公式, 如果A
2、B是永真式, 则称A 与B等值, 记作AB, 并称AB是等值式 基本等值式 第一组 命题逻辑中16组基本等值式的代换实例 例如，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) (5.1),2019/10/17,4,基本等值式,(2) 量词否定等值式 xA(x) xA(x) xA(x) xA(x) (5.2) (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) (5.3),2019/10/17,5,基本等值式,关于存在量词的： 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) (5.4) (4) 量词分配等值式 x(A(x)B(x) xA(x)xB(x) x(A(x)B(x) xA(x)xB(x) (5.5) 注意：对，对无分配律,2019/10/17,6,置换规则、换名规则、代替规则,1. 置换规则 设(A)是含A的公式, (B)是用公式B取代
4、(A) 中所有的A 之后得到的公式.那么, 若AB, 则(A)(B). 2. 换名规则 设A为一公式，将A中某量词辖域中一个约束变项的所有 出现及相应的指导变元换成该量词辖域中未曾出现过的个 体变项符号，其余部分不变，设所得公式为A，则AA. 3. 代替规则 设A为一公式，将A中某个自由出现的个体变项的所有出现 用A中未曾出现过的个体变项符号代替，其余部分不变，设所 得公式为A，则AA.,2019/10/17,7,实例,例1 将下面命题用两种形式符号化, 并证明两者等值: (1) 没有不犯错误的人,解 令F(x)：x是人，G(x)：x犯错误. x(F(x)G(x) 或 x(F(x)G(x),x
5、(F(x)G(x) x(F(x)G(x) 量词否定等值式 x(F(x)G(x) 置换 x(F(x)G(x) 置换,2019/10/17,8,实例,(2) 不是所有的人都爱看电影,解 令F(x)：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) 置换 x(F(x)G(x) 置换,2019/10/17,9,实例,(3)并不是所有的兔子都比乌龟跑得快.,设F(x): x是兔子,G(y):y是乌龟, H(x,y): x比y跑得快,xy(F(x)G(y)H(x,y),或 xy(F(x) G(y)
6、 H(x,y),(4) P65 5.(3) (4),2019/10/17,10,实例,例2 将公式化成等值的不含既有约束出现、又有自由出现 的个体变项: (1) xF(x,y,z)yG(x,y,z) (2) x(F(x,y,z)yG(x,y,z),解 (1) x(F(x,y,z)yG(x,y,z) tF(t,y,z)yG(x,y,z) 换名规则 t(F(t,y,z)wG(x,w,z) 换名规则,或者 xF(x,y,z)yG(x,y,z) xF(x,t,z)yG(x,y,z) 代替规则 xF(x,t,z)yG(w,y,z) 代替规则,2019/10/17,11,实例,(2) x(F(x,y,z)
7、yG(x,y,z) x(F(x,y,z)tG(x,t,z) 换名规则 xt(F(x,y,z)G(x,t,z) 辖域扩张等值式,或者 x(F(x,y,z)yG(x,y,z) x(F(x,u,z)yG(x,y,z) 代替规则 xy(F(x,u,z)G(x,y,z) 辖域扩张等值式,2019/10/17,12,实例,例3 设个体域D=a,b,c, 消去下述公式中的量词: (1) xy(F(x)G(y),解 xy(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
8、(c) (F(c)G(a)(F(c)G(b)(F(c)G(c),2019/10/17,13,实例,解法二 xy(F(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),2019/10/17,14,实例,(2) xyF(x,y),xyF(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),2019/10/17,15,5.2 一阶逻辑
9、前束范式,定义5.2 设A为一个一阶逻辑公式，若A具有如下形式 Q1x1Q2x2QkxkB 则称A为前束范式，其中Qi (1 i k)为或，B为不含量词 的公式. 例如， x(F(x)G(x) xy(F(x)(G(y)H(x,y) 是前束范式 而 x(F(x)G(x) x(F(x)y(G(y)H(x,y) 不是前束范式，,2019/10/17,16,前束范式存在定理,定理5.1（前束范式存在定理） 一阶逻辑中的任何公式都存在与之等值的前束范式,例4 求下列公式的前束范式 (1) x(M(x)F(x),解 x(M(x)F(x) x(M(x)F(x) （量词否定等值式） x(M(x)F(x) 后两
10、步结果都是前束范式，说明公式的前束范式不惟一.,2019/10/17,17,求前束范式的实例,(2) xF(x)xG(x),解 xF(x)xG(x) xF(x)xG(x) （量词否定等值式） x(F(x)G(x) （量词分配等值式）,或 xF(x)xG(x) xF(x)xG(x) 量词否定等值式 xF(x)yG(y) 换名规则 xy(F(x)G(y) 辖域收缩扩张规则,2019/10/17,18,求前束范式的实例,(3) xF(x)y(G(x,y)H(y),或 xF(x)y(G(z,y)H(y) 代替规则 xy(F(x)(G(z,y)H(y),解 xF(x)y(G(x,y)H(y) zF(z)
11、y(G(x,y)H(y) 换名规则 zy(F(z)(G(x,y)H(y) 辖域收缩扩张规则,2019/10/17,19,5.3 一阶逻辑的推论理论,推理的形式结构 1. A1A2Ak B 若此式是永真式, 则称推理正确, 记作A1A2Ak B 2. 前提: A1, A2, Ak 结论: B 推理定理: 永真式的蕴涵式,2019/10/17,20,推理定理,第一组 命题逻辑推理定理的代换实例 如, xF(x)yG(y) xF(x) 第二组 基本等值式生成的推理定理 如, xF(x) xF(x), xF(x) xF(x) xF(x)xF(x), xF(x) xF(x) 第三组 其他常用推理定律 (
12、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) xA(x)xB(x) (4) x(A(x)B(x) xA(x)xB(x),2019/10/17,21,量词消去引入规则,1. 全称量词消去规则(-) 或 其中x,y是个体变项符号, c是个体常项符号, 且在A中x不在y 和y的辖域内自由出现. 2. 全称量词引入规则(+) 其中x是个体变项符号, 且不在前提的任何公式中自由出现,2019/10/17,22,量词消去引入规则,3. 存在量词消去规则(-) 其中x是个体变项符号, 且不在前提的任何公式和B中自由 出现,2
13、019/10/17,23,量词消去引入规则,4. 存在量词引入规则(+) 或 或 其中x,y是个体变项符号, c是个体常项符号, 且在A中y和c不在 x和x的辖域内自由出现.,2019/10/17,24,自然推理系统NL,定义5.3 自然推理系统NL 定义如下: 1. 字母表. 同一阶语言L 的字母表 2. 合式公式. 同L 的合式公式 3. 推理规则: (1) 前提引入规则 (2) 结论引入规则 (3) 置换规则 (4) 假言推理规则 (5) 附加规则 (6) 化简规则 (7) 拒取式规则,2019/10/17,25,自然推理系统NL,(8) 假言三段论规则 (9) 析取三段论规则 (10) 构造性二难推理规则 (11) 合取引入规则 (12) -规则 (13) +规则 (14) -规则 (15) +规则 推理的证明,2019/10/17,26,构造推理证明的实例,例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)
