《第5章一阶逻辑等值演算与推理剖析》由会员分享，可在线阅读，更多相关《第5章一阶逻辑等值演算与推理剖析（27页珍藏版）》请在金锄头文库上搜索。
1、1,主要内容 一阶逻辑等值式与基本的等值式 置换规则、换名规则、代替规则 前束范式 自然推理系统NL 及其推理规则,第五章 一阶逻辑等值演算与推理,2,5.1 一阶逻辑等值式与置换规则,定义5.1 设A, B是两个谓词公式, 如果AB是永真式, 则称A与B等值, 记作AB, 并称AB是等值式 基本等值式 第一组 命题逻辑中16组基本等值式的代换实例 例如，xF(x)xF(x), xF(x)yG(y) xF(x)yG(y) 等,3,3,基本等值式,双重否定律 A(x)A(x) 幂等律 A(x)A(x)A(x), A(x)A(x)A(x) 交换律 A(x)B(x)B(x)A(x), A(x)B(x
2、)B(x)A(x) 结合律 (A(x)B(x)C(x)A(x)(B(x)C(x), (A(x)B(x)C(x)A(x)(B(x)C(x) 分配律 A(x)(B(x)C(x)(A(x)B(x)(A(x)C(x) A(x)(B(x)C(x)(A(x)B(x)(A(x)C(x) 德摩根律 (A(x)B(x)A(x)B(x) (A(x)B(x)A(x)B(x) 吸收律 A(x)(A(x)B(x)A(x) A(x)(A(x)B(x)A(x),4,4,基本等值式,零律 A(x)11, A(x)00 同一律 A(x)0A(x). A(x)1A(x) 排中律 A(x)A(x)1 矛盾律 A(x)A(x)0 蕴
3、涵等值式 A(x)B(x)A(x)B(x) 等价等值式 A(x)B(x)(A(x)B(x)(B(x)A(x) 假言易位 A(x)B(x)B(x)A(x) 等价否定等值式 A(x)B(x)A(x)B(x) 归谬论 (A(x)B(x)(A(x)B(x) A(x),5,第二组 (1) 消去量词等值式 设D =a1, a2, , an xA(x) A(a1)A(a2)A(an) xA(x) A(a1)A(a2)A(an),6,(2) 量词否定等值式 xA(x) xA(x) xA(x) xA(x) 例 不是所有的人都喜欢吃糖。 没有人喜欢吃糖。 设个体域D:人类集合 F(x): x是人, G(x): x
4、喜欢吃糖,7,证明 设个体域 ,则,8,基本等值式,(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),9,基本等值式,关于存在量词的： 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),10,基本等值式,(4) 量词分配等值式 x(A(x)B(x) xA(x)xB(x) x(A(x)B(x) xA(x)xB(x) 注意：对，对无
5、分配律,11,置换规则、换名规则、代替规则,1. 置换规则 设(A)是含A的公式, 那么, 若AB, 则(A)(B). 2. 换名规则 设A为一公式，将A中某量词辖域中个体变项的所有约束出现及相应的指导变元换成该量词辖域中未曾出现过的个体变项符号，其余部分不变，设所得公式为A，则AA. 3. 代替规则 设A为一公式，将A中某个个体变项的所有自由出现用A中未曾出现过的个体变项符号代替，其余部分不变，设所得公式为A，则AA.,12,实例,例1 将下面命题用两种形式符号化, 并证明两者等值: (1) 没有不犯错误的人,解 令F(x)：x是人，G(x)：x犯错误. x(F(x)G(x) 或 x(F(x
6、)G(x),x(F(x)G(x) x(F(x)G(x) 量词否定等值式 x(F(x)G(x) 置换 x(F(x)G(x) 置换,13,实例,(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) 置换,14,实例,例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(
7、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) 辖域扩张等值式,15,实例,例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),16,实例,解法二 xy(F(x)
8、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),17,实例,(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),18,5.2 一阶逻辑前束范式,定义5.2 设A为一个一阶逻辑公式，若A具有如下形式 Q1x1Q2x2QkxkB 则称A为前束范式，其中Qi (1 i k)为或，B为不含量词的公式。 例
9、如， 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) 不是前束范式，,19,前束范式存在定理,定理5.1（前束范式存在定理） 一阶逻辑中的任何公式都存在与之等值的前束范式,例4 求下列公式的前束范式 (1) x(M(x)F(x),解 x(M(x)F(x) x(M(x)F(x) （量词否定等值式） x(M(x)F(x) 后两步结果都是前束范式，说明公式的前束范式不惟一。,20,求前束范式的实例,(2) xF(x)xG(x),解 xF(x)xG(x) xF(x)xG(x) （量词否定等值式） x(F(x)G(x
10、) （量词分配等值式）,或 xF(x)xG(x) xF(x)xG(x) 量词否定等值式 xF(x)yG(y) 换名规则 xy(F(x)G(y) 辖域收缩扩张规则,21,求前束范式的实例,(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) 辖域收缩扩张规则,22,5.3 一阶逻辑的推理理论,一、推理的形式结构 1. A1A2Ak B 若此式是永真式, 则称推理正确, 记作A1A2Ak B 2.
11、前提: A1, A2, Ak 结论: B 推理定理: 永真式的蕴涵式,23,二、谓词逻辑推理定律 第一组：命题逻辑推理定律的代换实例都是谓词逻辑的推理定律。 如：x F(x)y G(y)x F(x) x F(x) x F(x)y G(y),24,第二组：由基本等值式生成的推理定律。每个等值式可生成两个推理定律。 如：由量词否定等值式 xA(x) xA(x)生成两个定律： x A(x) x A(x)， x A(x) x A(x),25,由量词辖域扩张等值式 x(A(x)B) xA(x)B 生成： x(A(x)B) x A(x)B , xA(x)B x(A(x)B) 由量词分配等值式 x(A(x)
12、B(x) xA(x)xB(x) 生成： x(A(x)B(x) xA(x)xB(x), xA(x)xB(x) x(A(x)B(x),26,第三组：其它重要推理定律。如： (1) x A(x)x B(x) x(A(x)B(x) (2) x(A(x)B(x) x A(x)x B(x) (3) x(A(x)B(x) xA(x)x B(x) (4) x(A(x)B(x) x A(x)x B(x),27,全称量词对，存在量词对不满足分配律。 例：个体域是人的集合。 A(x)：x是女人。 B(x)：x是男人。 为真； 为假。 为假； 为真。 仅满足：,28,在谓词逻辑中，除了命题逻辑中的推理规则继续有效外，
13、还有以下四条规则。设前提= A1,A2,Ak。（只对前束范式有用） 1. 全称量词消去规则（记为 -）：,三、谓词逻辑推理规则,其中x,y是个体变项符号，c是个体常项符号；,或, A(y), A(c),且在A中x不在 y和 y的辖域内自由出现。,29,2 . 全称量词引入规则 (记为+)：,三、谓词逻辑推理规则,其中x是个体变项符号，且不在的任何公式中自由出现。, x A(x),30,三、谓词逻辑推理规则,3. 存在量词消去规则 (记为-)：,其中c是使A为真的特定的个体常项。 x是个体变项符号，且不在的任何公式和B中自由出现。, xA(x)B,A(c),或,31,4. 存在量词引入规则 (记为+)：,三、谓词逻辑推理规则,其中x,y是个体变项符号, c是个体常项符号, 并且在A中y和 c分别不在x 和x的辖域内自由出现。, BxA(x), xA(x),或, BxA(x
