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