离散数学(第2.5)陈瑜

陈瑜Email：chenyu.inbox@gmail11/20/2023离散数学计算机学院1/8/20241计算机科学与工程学院主要内容1.谓词逻辑的推理方法2.消解(归结)法1/8/20242计算机科学与工程学院2.5谓词逻辑的推理推理演算过程：①首先将以自然语句表示的推理问题引入谓词加以形式化；★②假设不能直接使用根本推理公式那么消去量词；③在无量词的情形下使用推理规那么和公式进行推理；④最后再引入量词以求得结论。

1/8/20243计算机科学与工程学院推理规那么命题逻辑推理的三条推理规那么继续实用于谓词逻辑推理！〔P、T、CP〕在前面介绍的推理演算过程中，如何消去量词或引入量词？下面介绍4条专门针对量词的推理规那么。1/8/20244计算机科学与工程学院推理规那么命题逻辑推理的三条推理规那么继续实用于谓词逻辑推理！〔P、T、CP〕在前面介绍的推理演算过程中，如何消去量词或引入量词？下面介绍4条专门针对量词的推理规那么。1/8/20245计算机科学与工程学院推理规那么量词的四条重要的推理规那么：1)US规那么(全称指定规那么、全称量词消去规那么)： (x)G(x)G(y)①或(x)G(x)G(c)②注意：以上2公式的成立条件：1〕y是任意的不在G〔x〕中受约束出现的个体变项；2〕c为任意个体变项；US规那么说明“每一个均成立，那么其中任一个也必成立〞。

1/8/20246计算机科学与工程学院推理规那么量词的四条重要的推理规那么：1)US规那么(全称指定规那么、全称量词消去规那么)： (x)G(x)G(y)①或(x)G(x)G(c)②注意：以上2公式的成立条件：1〕y是任意的不在G〔x〕中受约束出现的个体变项；2〕c为任意个体变项；US规那么说明“每一个均成立，那么其中任一个也必成立〞。1/8/20247计算机科学与工程学院推理规那么2)UG规那么(全称推广规那么、全称量词附加规那么)： G(y)(x)G(x)注意：以上公式的成立条件：1〕y在G〔x〕中自由出现，并且y取任意y∈D时，G〔y〕为真；2〕取代y的x不能在G〔y〕中出现；3〕US规那么不是UG规那么的逆命题；4〕US规那么中y是“某一个〞，而UG规那么中的y是“每一个〞。

1/8/20248计算机科学与工程学院推理规那么2)UG规那么(全称推广规那么、全称量词附加规那么)： G(y)(x)G(x)注意：以上公式的成立条件：1〕y在G〔x〕中自由出现，并且y取任意y∈D时，G〔y〕均为真；2〕取代y的x不能在G〔y〕中出现；3〕US规那么不是UG规那么的逆命题；4〕US规那么中y是“某一个〞，而UG规那么中的y是“每一个〞。

1/8/20249计算机科学与工程学院推理规那么3)ES规那么(存在指定规那么、存在量词消去规那么)： 〔x)G(x〕G〔c〕注意：以上公式的成立条件：1〕c是使G〔x〕为真的特定的个体常项；2〕c不曾在G〔x〕中出现过；3〕G〔x〕中除x外，还有其他自由变项时，不可用此规那么；尤其第一条，c不是任取一个，而是某些特定的个体！例：G〔x〕：x是男生，c：王芳。那么：〔x)G(x〕G〔c〕是错误的推理！

1/8/202410计算机科学与工程学院推理规那么3)ES规那么(存在指定规那么、存在量词消去规那么)： 〔x)G(x〕G〔c〕注意：以上公式的成立条件：1〕c是使G〔x〕为真的特定的个体常项；2〕c不曾在G〔x〕中出现过；3〕G〔x〕中除x外，还有其他自由变项时，不可用此规那么；尤其第一条，c不是任取一个，而是某些特定的个体！例：G〔x〕：x是男生，c：王芳。那么：〔x)G(x〕G〔c〕是错误的推理！

1/8/202411计算机科学与工程学院推理规那么3)ES规那么(存在指定规那么、存在量词消去规那么)： 〔x)G(x〕G〔c〕注意：以上公式的成立条件：1〕c是使G〔x〕为真的特定的个体常项；2〕c不曾在G〔x〕中出现过；3〕G〔x〕中除x外，还有其他自由变项时，不可用此规那么；尤其第一条，c不是任取一个，而是某些特定的个体！例：G〔x〕：x是男生，c：王芳。那么：〔x)G(x〕G〔c〕是错误的推理！

1/8/202412计算机科学与工程学院推理规那么4)EG规那么(存在推广规那么、存在量词附加规那么)： G〔c〕〔x)G(x〕注意：以上公式的成立条件：1〕c是某个个体常项；2〕取代c的x不能在G〔c〕中出现过；

1/8/202413计算机科学与工程学院推理方法1〕直接证明法2〕CP规那么证明法3〕反证法等。1/8/202414计算机科学与工程学院例5-1：证明论断“人都是要死的，苏格拉底是人，所以苏格拉底是要死的〞的正确性。证：设谓词Man〔x〕：x是人；Mortal〔x〕：x是要死的；客体s：苏格拉底。那么以上论断符号化为：(x)[Man(x)Mortal(x)]∧Man(s)Mortal(s)

1/8/202415计算机科学与工程学院例5-1：证明论断“人都是要死的，苏格拉底是人，所以苏格拉底是要死的〞的正确性。证：设谓词Man〔x〕：x是人；Mortal〔x〕：x是要死的；客体s：苏格拉底。那么以上论断符号化为：(x)[Man(x)Mortal(x)]∧Man(s)Mortal(s)

1/8/202416计算机科学与工程学院证:(续)〔直接证明法可采用如下步骤进行〕1)(x)[Man(x)Mortal(x)]P2)Man(s)Mortal(s)US1)3)Man(s)P4)Mortal(s)T(2,3)I3

1/8/202417计算机科学与工程学院例：〔p40例2.19〕1/8/202418计算机科学与工程学院例5-2：试证(x)(C(x)W(x)∧R(x))∧(x)(C(x)∧Q(x))〔x〕(Q(x)∧R(x))分析：前提：(x)(C(x)W(x〕∧R(x))，〔x〕(C(x)∧Q(x))结论：〔x〕(Q(x)∧R(x))思路：在使用前提时，尽量先使用前提。因为成立，即有一个特定的个体c存在，并且c对前提中每个个体均成立，但反之不一定成立。1/8/202419计算机科学与工程学院例5-2：试证(x)(C(x)W(x)∧R(x))∧(x)(C(x)∧Q(x))〔x〕(Q(x)∧R(x))分析：前提：(x)(C(x)W(x〕∧R(x))，〔x〕(C(x)∧Q(x))结论：〔x〕(Q(x)∧R(x))思路：在使用前提时，尽量先使用前提。因为成立，即有一个特定的个体c存在，并且c对前提中每个个体均成立，但反之不一定成立。1/8/202420计算机科学与工程学院例5-2：试证(x)(C(x)W(x)∧R(x))∧(x)(C(x)∧Q(x))〔x〕(Q(x)∧R(x))分析：前提：(x)(C(x)W(x〕∧R(x))，〔x〕(C(x)∧Q(x))结论：〔x〕(Q(x)∧R(x))思路：在使用前提时，尽量先使用前提。因为成立，即有一个特定的个体c存在，并且c对前提中每个个体均成立，但反之不一定成立。1/8/202421计算机科学与工程学院证明：〔1〕〔x〕(C(x)∧Q(x))P〔2〕C(a)∧Q(a)ES(1)(注：此处a是特定的〕〔3〕(x)(C(x)W(x〕∧R(x))P〔4〕C(a)W(a〕∧R(a))US〔3〕〔注：因〔3〕中“任意〞的，所以此处可以使用(2)中的a。假设〔3〕中是，那么此处不可用a。〕〔5〕C(a)T(2)I21/8/202422计算机科学与工程学院证明：〔1〕〔x〕(C(x)∧Q(x))P〔2〕C(a)∧Q(a)ES(1)(注：此处a是特定的〕〔3〕(x)(C(x)W(x〕∧R(x))P〔4〕C(a)W(a〕∧R(a))US〔3〕〔注：因〔3〕中“任意〞的，所以此处可以使用(2)中的a。假设〔3〕中是，那么此处不可用a。〕〔5〕C(a)T(2)I21/8/202423计算机科学与工程学院证明：〔1〕〔x〕(C(x)∧Q(x))P〔2〕C(a)∧Q(a)ES(1)(注：此处a是特定的〕〔3〕(x)(C(x)W(x〕∧R(x))P〔4〕C(a)W(a〕∧R(a))US〔3〕〔注：因〔3〕中“任意〞的，所以此处可以使用(2)中的a。假设〔3〕中是，那么此处不可用a。〕〔5〕C(a)T(2)I21/8/202424计算机科学与工程学院证明：〔1〕〔x〕(C(x)∧Q(x))P〔2〕C(a)∧Q(a)ES(1)(注：此处a是特定的〕〔3〕(x)(C(x)W(x〕∧R(x))P〔4〕C(a)W(a〕∧R(a))US〔3〕〔注：因〔3〕中“任意〞的，所以此处可以使用(2)中的a。假设〔3〕中是，那么此处不可用a。〕〔5〕C(a)T(2)I21/8/202425计算机科学与工程学院证明：〔1〕〔x〕(C(x)∧Q(x))P〔2〕C(a)∧Q(a)ES(1)(注：此处a是特定的〕〔3〕(x)(C(x)W(x〕∧R(x))P〔4〕C(a)W(a〕∧R(a))US〔3〕〔注：因〔3〕中“任意〞的，所以此处可以使用(2)中的a。假设〔3〕中是，那么此处不可用a。〕〔5〕C(a)T(2)I21/8/202426计算机科学与工程学院证明〔续〕：〔6〕W(a〕∧R(a)T(4)(5)I3〔7〕R(a)T(6)I2〔8〕Q(a)T(2)I2〔9〕Q(a〕∧R(a)T(7)(8)I1〔10〕〔x〕(Q(x)∧R(x))EG(9)证毕■

1/8/202427计算机科学与工程学院证明〔续〕：〔6〕W(a〕∧R(a)T(4)(5)I3〔7〕R(a)T(6)I2〔8〕Q(a)T(2)I2〔9〕Q(a〕∧R(a)T(7)(8)I1〔10〕〔x〕(Q(x)∧R(x))EG(9)证毕■

1/8/202428计算机科学与工程学院证明〔续〕：〔6〕W(a〕∧R(a)T(4)(5)I3〔7〕R(a)T(6)I2〔8〕Q(a)T(2)I2〔9〕Q(a〕∧R(a)T(7)(8)I1〔10〕〔x〕(Q(x)∧R(x))EG(9)证毕■

1/8/202429计算机科学与工程学院证明〔续〕：〔6〕W(a〕∧R(a)T(4)(5)I3〔7〕R(a)T(6)I2〔8〕Q(a)T(2)I2〔9〕Q(a〕∧R(a)T(7)(8)I1〔10〕〔x〕(Q(x)∧R(x))EG(9)证毕■

1/8/202430计算机科学与工程学院证明〔续〕：〔6〕W(a〕∧R(a)T(4)(5)I3〔7〕R(a)T(6)I2〔8〕Q(a)T(2)I2〔9〕Q(a〕∧R(a)T(7)(8)I1〔10〕〔x〕(Q(x)∧R(x))EG(9)证毕■

1/8/202431计算机科学与工程学院例5-3：试证明：前提：～(x)(F(x)∧H(x)),(x)(G(x)H(x))结论：(x)(G(x)～F(x))证明：～(x)(F(x)∧H(x))P(2)(x)(～F(x)∨～H(x))T(1)E(3)(x)(H(x)～F(x))T(2)E(4)H(y)～F(y)US(3)(5)(x)(G(x)H(x))PG(y)H(y)US(5)(7)G(y)～F(y)T(4)(6)I6(8)(x)(G(x)～F(x))UG(7)证毕■(因为〔7〕中y指代任意的)1/8/202432计算机科学与工程学院例5-3：试证明：前提：～(x)(F(x)∧H(x)),(x)(G(x)H(x))结论：(x)(G(x)～F(x))证明：～(x)(F(x)∧H(x))P(2)(x)(～F(x)∨～H(x))T(1)E(3)(x)(H(x)～F(x))T(2)E(4)H(y)～F(y)US(3)(5)(x)(G(x)H(x))PG(y)H(y)US(5)(7)G(y)～F(y)T(4)(6)I6(8)(x)(G(x)～F(x))UG(7)证毕■(因为〔7〕中y指代任意的)1/8/202433计算机科学与工程学院例5-3：试证明：前提：～(x)(F(x)∧H(x)),(x)(G(x)H(x))结论：(x)(G(x)～F(x))证明：～(x)(F(x)∧H(x))P(2)(x)(～F(x)∨～H(x))T(1)E(3)(x)(H(x)～F(x))T(2)E(4)H(y)～F(y)US(3)(5)(x)(G(x)H(x))PG(y)H(y)US(5)(7)G(y)～F(y)T(4)(6)I6(8)(x)(G(x)～F(x))UG(7)证毕■(因为〔7〕中y指代任意的)1/8/202434计算机科学与工程学院例5-3：试证明：前提：～(x)(F(x)∧H(x)),(x)(G(x)H(x))结论：(x)(G(x)～F(x))证明：～(x)(F(x)∧H(x))P(2)(x)(～F(x)∨～H(x))T(1)E(3)(x)(H(x)～F(x))T(2)E(4)H(y)～F(y)US(3)(5)(x)(G(x)H(x))PG(y)H(y)US(5)(7)G(y)～F(y)T(4)(6)I6(8)(x)(G(x)～F(x))UG(7)证毕■(因为〔7〕中y指代任意的)1/8/202435计算机科学与工程学院例5-3：试证明：前提：～(x)(F(x)∧H(x)),(x)(G(x)H(x))结论：(x)(G(x)～F(x))证明：～(x)(F(x)∧H(x))P(2)(x)(～F(x)∨～H(x))T(1)E(3)(x)(H(x)～F(x))T(2)E(4)H(y)～F(y)US(3)(5)(x)(G(x)H(x))PG(y)H(y)US(5)(7)G(y)～F(y)T(4)(6)I6(8)(x)(G(x)～F(x))UG(7)证毕■(因为〔7〕中y指代任意的)1/8/202436计算机科学与工程学院例5-3：试证明：前提：～(x)(F(x)∧H(x)),(x)(G(x)H(x))结论：(x)(G(x)～F(x))证明：～(x)(F(x)∧H(x))P(2)(x)(～F(x)∨～H(x))T(1)E(3)(x)(H(x)～F(x))T(2)E(4)H(y)～F(y)US(3)(5)(x)(G(x)H(x))PG(y)H(y)US(5)(7)G(y)～F(y)T(4)(6)I6(8)(x)(G(x)～F(x))UG(7)证毕■(因为〔7〕中y指代任意的)1/8/202437计算机科学与工程学院例5-3：试证明：前提：～(x)(F(x)∧H(x)),(x)(G(x)H(x))结论：(x)(G(x)～F(x))证明：～(x)(F(x)∧H(x))P(2)(x)(～F(x)∨～H(x))T(1)E(3)(x)(H(x)～F(x))T(2)E(4)H(y)～F(y)US(3)(5)(x)(G(x)H(x))PG(y)H(y)US(5)(7)G(y)～F(y)T(4)(6)I6(8)(x)(G(x)～F(x))UG(7)证毕■(因为〔7〕中y指代任意的)1/8/202438计算机科学与工程学院例5-3：试证明：前提：～(x)(F(x)∧H(x)),(x)(G(x)H(x))结论：(x)(G(x)～F(x))证明：～(x)(F(x)∧H(x))P(2)(x)(～F(x)∨～H(x))T(1)E(3)(x)(H(x)～F(x))T(2)E(4)H(y)～F(y)US(3)(5)(x)(G(x)H(x))PG(y)H(y)US(5)(7)G(y)～F(y)T(4)(6)I6(8)(x)(G(x)～F(x))UG(7)证毕■(因为〔7〕中y指代任意的)1/8/202439计算机科学与工程学院例5-3：试证明：前提：～(x)(F(x)∧H(x)),(x)(G(x)H(x))结论：(x)(G(x)～F(x))证明：～(x)(F(x)∧H(x))P(2)(x)(～F(x)∨～H(x))T(1)E(3)(x)(H(x)～F(x))T(2)E(4)H(y)～F(y)US(3)(5)(x)(G(x)H(x))PG(y)H(y)US(5)(7)G(y)～F(y)T(4)(6)I6(8)(x)(G(x)～F(x))UG(7)证毕■(因为〔7〕中y指代任意的)1/8/202440计算机科学与工程学院例5-4：“有些病人相信所有的医生，而病人均不相信江湖骗子〞。试证明“医生不是骗子〞。符号化：R(x):x是病人D(x):x是医生S(x):x是江湖骗子L(x,y):x相信y前提：(x)(R(x)∧(y)(D(y〕L(x,y))),(x)(R(x)(y)(S(y〕～L(x,y)))结论：(x)(D(x)～S(x))思路：先用再用，即先找特殊的再找一般的！1/8/202441计算机科学与工程学院例5-4：“有些病人相信所有的医生，而病人均不相信江湖骗子〞。试证明“医生不是骗子〞。符号化：R(x):x是病人D(x):x是医生S(x):x是江湖骗子L(x,y):x相信y前提：(x)(R(x)∧(y)(D(y〕L(x,y))),(x)(R(x)(y)(S(y〕～L(x,y)))结论：(x)(D(x)～S(x))思路：先用再用，即先找特殊的再找一般的！1/8/202442计算机科学与工程学院例5-4：“有些病人相信所有的医生，而病人均不相信江湖骗子〞。试证明“医生不是骗子〞。符号化：R(x):x是病人D(x):x是医生S(x):x是江湖骗子L(x,y):x相信y前提：(x)(R(x)∧(y)(D(y〕L(x,y))),(x)(R(x)(y)(S(y〕～L(x,y)))结论：(x)(D(x)～S(x))思路：先用再用，即先找特殊的再找一般的！1/8/202443计算机科学与工程学院例5-4：“有些病人相信所有的医生，而病人均不相信江湖骗子〞。试证明“医生不是骗子〞。符号化：R(x):x是病人D(x):x是医生S(x):x是江湖骗子L(x,y):x相信y前提：(x)(R(x)∧(y)(D(y〕L(x,y))),(x)(R(x)(y)(S(y〕～L(x,y)))结论：(x)(D(x)～S(x))思路：先用再用，即先找特殊的再找一般的！1/8/202444计算机科学与工程学院证明：(1)(x)(R(x)∧(y)(D(y〕L(x,y)))P(2)R(a)∧(y)(D(y〕L(a,y))ES(1)(a是相信所有医生的那个人)(3)(y)(D(y〕L(a,y))T(2)I2(4)D(t〕L(a,t)US〔3〕(此处t是所有的人，与〔2〕中a不同)(5)(x)(R(x)(y)(S(y)～L(x,y)))P(6)R(a)(y)(S(y)～L(a,y)))US(5)(注意此处的a：既然(5)中指所有的人，那么就应包括(2)中的那个特定的人〕(7)R(a)T(2)I21/8/202445计算机科学与工程学院证明：(1)(x)(R(x)∧(y)(D(y〕L(x,y)))P(2)R(a)∧(y)(D(y〕L(a,y))ES(1)(a是相信所有医生的那个人)(3)(y)(D(y〕L(a,y))T(2)I2(4)D(t〕L(a,t)US〔3〕(此处t是所有的人，与〔2〕中a不同)(5)(x)(R(x)(y)(S(y)～L(x,y)))P(6)R(a)(y)(S(y)～L(a,y)))US(5)(注意此处的a：既然(5)中指所有的人，那么就应包括(2)中的那个特定的人〕(7)R(a)T(2)I21/8/202446计算机科学与工程学院证明：(1)(x)(R(x)∧(y)(D(y〕L(x,y)))P(2)R(a)∧(y)(D(y〕L(a,y))ES(1)(a是相信所有医生的那个人)(3)(y)(D(y〕L(a,y))T(2)I2(4)D(t〕L(a,t)US〔3〕(此处t是所有的人，与〔2〕中a不同)(5)(x)(R(x)(y)(S(y)～L(x,y)))P(6)R(a)(y)(S(y)～L(a,y)))US(5)(注意此处的a：既然(5)中指所有的人，那么就应包括(2)中的那个特定的人〕(7)R(a)T(2)I21/8/202447计算机科学与工程学院证明：(1)(x)(R(x)∧(y)(D(y〕L(x,y)))P(2)R(a)∧(y)(D(y〕L(a,y))ES(1)(a是相信所有医生的那个人)(3)(y)(D(y〕L(a,y))T(2)I2(4)D(t〕L(a,t)US〔3〕(此处t是所有的人，与〔2〕中a不同)(5)(x)(R(x)(y)(S(y)～L(x,y)))P(6)R(a)(y)(S(y)～L(a,y)))US(5)(注意此处的a：既然(5)中指所有的人，那么就应包括(2)中的那个特定的人〕(7)R(a)T(2)I21/8/202448计算机科学与工程学院证明：(1)(x)(R(x)∧(y)(D(y〕L(x,y)))P(2)R(a)∧(y)(D(y〕L(a,y))ES(1)(a是相信所有医生的那个人)(3)(y)(D(y〕L(a,y))T(2)I2(4)D(t〕L(a,t)US〔3〕(此处t是所有的人，与〔2〕中a不同)(5)(x)(R(x)(y)(S(y)～L(x,y)))P(6)R(a)(y)(S(y)～L(a,y)))US(5)(注意此处的a：既然(5)中指所有的人，那么就应包括(2)中的那个特定的人〕(7)R(a)T(2)I21/8/202449计算机科学与工程学院证明：(1)(x)(R(x)∧(y)(D(y〕L(x,y)))P(2)R(a)∧(y)(D(y〕L(a,y))ES(1)(a是相信所有医生的那个人)(3)(y)(D(y〕L(a,y))T(2)I2(4)D(t〕L(a,t)US〔3〕(此处t是所有的人，与〔2〕中a不同)(5)(x)(R(x)(y)(S(y)～L(x,y)))P(6)R(a)(y)(S(y)～L(a,y)))US(5)(注意此处的a：既然(5)中指所有的人，那么就应包括(2)中的那个特定的人〕(7)R(a)T(2)I21/8/202450计算机科学与工程学院证明：(1)(x)(R(x)∧(y)(D(y〕L(x,y)))P(2)R(a)∧(y)(D(y〕L(a,y))ES(1)(a是相信所有医生的那个人)(3)(y)(D(y〕L(a,y))T(2)I2(4)D(t〕L(a,t)US〔3〕(此处t是所有的人，与〔2〕中a不同)(5)(x)(R(x)(y)(S(y)～L(x,y)))P(6)R(a)(y)(S(y)～L(a,y)))US(5)(注意此处的a：既然(5)中指所有的人，那么就应包括(2)中的那个特定的人〕(7)R(a)T(2)I21/8/202451计算机科学与工程学院证明：(8)(y)(S(y)～L(a,y))T(6)(7)I3(9)S(t)～L(a,t)US(8)(10)L(a,t)～S(t)T(9)E22(11)D(t)～S(t)T(4)(10)I6(12)(x)(D(x)～S(x))UG(11)证毕■(因为(11)中的t指代的是任意的人！)

1/8/202452计算机科学与工程学院证明：(8)(y)(S(y)～L(a,y))T(6)(7)I3(9)

S(t)～L(a,t)US(8)(10)L(a,t)～S(t)T(9)E22(11)D(t)～S(t)T(4)(10)I6(12)(x)(D(x)～S(x))UG(11)证毕■(因为(11)中的t指代的是任意的人！)

1/8/202453计算机科学与工程学院证明：(8)(y)(S(y)～L(a,y))T(6)(7)I3(9)

S(t)～L(a,t)US(8)(10)

L(a,t)～S(t)T(9)E22(11)D(t)～S(t)T(4)(10)I6(12)(x)(D(x)～S(x))UG(11)证毕■(因为(11)中的t指代的是任意的人！)

1/8/202454计算机科学与工程学院证明：(8)(y)(S(y)～L(a,y))T(6)(7)I3(9)

S(t)～L(a,t)US(8)(10)

L(a,t)～S(t)T(9)E22(11)D(t)～S(t)T(4)(10)I6(12)(x)(D(x)～S(x))UG(11)证毕■(因为(11)中的t指代的是任意的人！)

1/8/202455计算机科学与工程学院证明：(8)(y)(S(y)～L(a,y))T(6)(7)I3(9)

S(t)～L(a,t)US(8)(10)

L(a,t)～S(t)T(9)E22(11)D(t)～S(t)T(4)(10)I6(12)

(x)(D(x)～S(x))UG(11)证毕■

(因为(11)中的t指代的是任意的人！)

1/8/202456计算机科学与工程学院消解(归结)法消解证明的过程：(1)为了证明

G1,G2,…,Gn

H

根据反证法，即需证明

G={G1,G2,…,Gn,～H}

R∧～R(2)建立子句集①先将G化成等值的前束范式②将前束范式化成Skolem范式(消去存在量词),得到仅含全称量词的公式G*,从而对G的不可满足性,可由G*的不可满足性得到。

1/8/202457计算机科学与工程学院消解(归结)法消解证明的过程：(1)为了证明

G1,G2,…,Gn

H根据反证法，即需证明G={G1,G2,…,Gn,～H}

R∧～R(2)建立子句集

①先将G化成等值的前束范式

②将前束范式化成Skolem范式(消去存在量词),得到仅含全称量词的公式G*,从而对G的不可满足性,可由G*的不可满足性得到。

1/8/202458计算机科学与工程学院消解(归结)法消解证明的过程：(1)为了证明

G1,G2,…,Gn

H根据反证法，即需证明G={G1,G2,…,Gn,～H}

R∧～R(2)建立子句集

①先将G化成等值的前束范式

②将前束范式化成Skolem范式(消去存在量词),得到仅含全称量词的公式G*,从而对G的不可满足性,可由G*的不可满足性得到。

1/8/202459计算机科学与工程学院消解(归结)法(续)

③将G*的全称量词省略。

④G*的母式(已合取化)的合取词‘

’以‘，’表示,得G的子句集S。(3)对S作归结(消解)归结：设C1,C1是两个无共同变元的子句,L1,L2分别是C1,C2中的句节。如果L1和～L2有合一置换(一致化)

(L1,L2中的变元x用

代入),(C1

-{L1

})U(C2

-{L2

})称作子句C1,C2的归结式。1/8/202460计算机科学与工程学院消解(归结)法(续)

③将G*的全称量词省略。

④G*的母式(已合取化)的合取词‘

’以‘，’表示,得G的子句集S。(3)对S作归结(消解)归结：设C1,C1是两个无共同变元的子句,L1,L2分别是C1,C2中的句节。如果L1和～L2有合一置换(一致化)

(L1,L2中的变元x用

代入),(C1

-{L1

})U(C2

-{L2

})称作子句C1,C2的归结式。1/8/202461计算机科学与工程学院消解(归结)法(续)③将G*的全称量词省略。④G*的母式(已合取化)的合取词‘

’以‘，’表示,得G的子句集S。(3)对S作归结(消解)

归结：设C1,C1是两个无共同变元的子句,L1,L2分别是C1,C2中的句节。如果L1和～L2有合一置换(一致化)

(L1,L2中的变元x用

代入),(C1

-{L1

})U(C2

-{L2

})称作子句C1,C2的归结式。1/8/202462计算机科学与工程学院消解(归结)法〔续〕〔例如C1=P(x)Q(x)C2=～P(a)R(y)P(x)与～P(a)合一置换{a/x},即将变元x换成a,便为互补对,可作归结了,有归结式R(C1,C2)=Q(a)R(y)〕对子句集S的任意两个子句作归结(如果可作归结)并将归结式仍放入S,重复这一过程。(4)直到归结出空子句□,证明结束。1/8/202463计算机科学与工程学院消解(归结)法〔续〕〔例如C1=P(x)Q(x)C2=～P(a)R(y)P(x)与～P(a)合一置换{a/x},即将变元x换成a,便为互补对,可作归结了,有归结式R(C1,C2)=Q(a)R(y)〕对子句集S的任意两个子句作归结(如果可作归结)并将归结式仍放入S,重复这一过程。(4)直到归结出空子句□,证明结束。1/8/202464计算机科学与工程学院消解(归结)法〔续〕〔例如C1=P(x)Q(x)C2=～P(a)R(y)P(x)与～P(a)合一置换{a/x},即将变元x换成a,便为互补对,可作归结了,有归结式R(C1,C2)=Q(a)R(y)〕对子句集S的任意两个子句作归结(如果可作归结)并将归结式仍放入S,重复这一过程。(4)直到归结出空子句□,证明结束。1/8/202465计算机科学与工程学院例5-5利用消解法证明:〔p42例2.22〕前提：(x)(P(x)(y)(Q(y)～R(x,y))),(x)(P(x)(y)(S(y)R(x,y)))结论：(x)(S(x)～Q(x))证明：首先将结论的否认作为附加前提，与原有前提一起转化为Skolem范式：(x)(P(x)(y)(Q(y)～R(x,y)))(x)(P(x)(y)(S(y)R(x,y)))～(x)(S(x)～Q(x))

1/8/202466计算机科学与工程学院例5-5利用消解法证明:〔p42例2.22〕前提：(x)(P(x)(y)(Q(y)～R(x,y))),(x)(P(x)(y)(S(y)R(x,y)))结论：(x)(S(x)～Q(x))证明：首先将结论的否认作为附加前提，与原有前提一起转化为Skolem范式：(x)(P(x)(y)(Q(y)～R(x,y)))(x)(P(x)(y)(S(y)R(x,y)))～(x)(S(x)～Q(x))

1/8/202467计算机科学与工程学院(x)(y)(～

P(x)∨

～Q(y)∨

～R(x,y))

(u)(P(u)(z)(～

S(z)∨R(u,z)))

(v)(S(v)

Q(v))(u)(v)(x)(y)(z)((～P(x)∨～Q(y)∨

～R(x,y))P(u)(～S(z)∨R(u,z))S(v)

Q(v)(x)(y)(z)((～P(x)∨～Q(y)∨

～R(x,y))P(a)(～S(z)∨R(a,z))S(b)

Q(b)①上面①即为Skolem范式，由此得到子句集：{～P(x)∨～Q(y)∨

～R(x,y)、P(a)、～S(z)∨R(a,z)、S(b)、Q(b)}。1/8/202468计算机科学与工程学院

(x)(y)(～P(x)∨～Q(y)∨

～R(x,y))

(u)(P(u)(z)(～S(z)∨R(u,z)))

(v)(S(v)

Q(v))

(u)(v)

(x)(y)(z)

[(～P(x)∨～Q(y)∨

～R(x,y))

P(u)(～S(z)∨R(u,z))

(S(v)

Q(v))](x)(y)(z)((～P(x)∨～Q(y)∨

～R(x,y))P(a)(～S(z)∨R(a,z))S(b)

Q(b)①上面①即为Skolem范式，由此得到子句集：{～P(x)∨～Q(y)∨

～R(x,y)、P(a)、～S(z)∨R(a,z)、S(b)、Q(b)}。1/8/202469计算机科学与工程学院

(x)(y)(～P(x)∨～Q(y)∨

～R(x,y))

(u)(P(u)(z)(～S(z)∨R(u,z)))(v)(S(v)

Q(v))(u)(v)(x)(y)(z)((～P(x)∨～Q(y)∨

～R(x,y))P(u)(～S(z)∨R(u,z))S(v)

Q(v)(x)(y)(z)((～P(x)∨～Q(y)∨

～R(x,y))

P(a)

(～

S(z)∨R(a,z))

S(b)

Q(b))

①

上面①即为Skolem范式，由此得到子句集：{～P(x)∨～Q(y)∨

～R(x,y)、P(a)、～S(z)∨R(a,z)、S(b)、Q(b)}。1/8/202470计算机科学与工程学院

(x)(y)(～P(x)∨～Q(y)∨

～R(x,y))

(u)(P(u)(z)(～S(z)∨R(u,z)))(v)(S(v)

Q(v))(u)(v)(x)(y)(z)((～P(x)∨～Q(y)∨

～R(x,y))P(u)(～S(z)∨R(u,z))S(v)

Q(v)(x)(y)(z)((～P(x)∨～Q(y)∨

～R(x,y))P(a)(～S(z)∨R(a,z))S(b)

Q(b)①

上面①即为Skolem范式，由此得到子句集：{～P(x)∨～Q(y)∨

～R(x,y)、P(a)、

～

S(z)∨R(a,z)、

S(b)、Q(b)}。1/8/202471计算机科学与工程学院然后，在此根底上利用代换进行消解的过程如下：(1)～P(x)∨～Q(y)∨～R(x,y)(2)P(a)(3)～Q(y)∨～R(a,y)(1)和(2),代换{a/x}(4)Q(b)(5)～R(a,b)(3)和(4),代换{b/y}(6)～S(z)∨R(a,z)(7)～S(b)(5)和(6),代换{b/z}(8)S(b)(9)□证毕■1/8/202472计算机科学与工程学院然后，在此根底上利用代换进行消解的过程如下：(1)～P(x)∨～Q(y)∨～R(x,y)(2)P(a)(3)～Q(y)∨～R(a,y)(1)和(2),代换{a/x}(4)Q(b)(5)～R(a,b)(3)和(4),代换{b/y}(6)～S(z)∨R(a,z)(7)～S(b)(5)和(6),代换{b/z}(8)S(b)(9)□证毕■1/8/202473计算机科学与工程学院然后，在此根底上利用代换进行消解的过程如下：(1)～P(x)∨～Q(y)∨～R(x,y)(2)P(a)(3)～Q(y)∨～R(a,y)(1)和(2),代换{a/x}(4)Q(b)(5)～R(a,b)(3)和(4),代换{b/y}(6)～S(z)∨R(a,z)(7)～S(b)(5)和(6),代换{b/z}(8)S(b)(9)□证毕■1/8/202474计算机科学与工程学院然后，在此根底上利用代换进行消解的过程如下：(1)～P(x)∨～Q(y)∨～R(x,y)(2)P(a)(3)～Q(y)∨～R(a,y)(1)和(2),代换{a/x}(4)Q(b)(5)～R(a,b)(3)和(4),代换{b/y}(6)～S(z)∨R(a,z)(7)～S(b)(5)和(6),代换{b/z}(8)S(b)(9)□证毕■1/8/202475计算机科学与工程学院然后，在此根底上利用代换进行消解的过程如下：(1)～P(x)∨～Q(y)∨～R(x,y)(2)P(a)(3)～Q(y)∨～R(a,y)(1)和(2),代换{a/x}(4)Q(b)(5)～R(a,b)(3)和(4),代换{b/y}(6)～S(z)∨R(a,z)(7)～S(b)(5)和(6),代换{b/z}(8)S(b)(9)□证毕■1/8/202476计算机科学与工程学院然后，在此根底上利用代换进行消解的过程如下：(1)～P(x)∨～Q(y)∨～R(x,y)(2)P(a)(3)～Q(y)∨～R(a,y)(1)和(2),代换{a/x}(4)Q(b)(5)～R(a,b)(3)和(4),代换{b/y}(6)～S(z)∨R(a,z)(7)～S(b)(5)和(6),代换{b/z}(8)S(b)(9)□证毕■1/8/202477计算机科学与工程学院然后，在此根底上利用代换进行消解的过程如下：(1)～P(x)∨～Q(y)∨～R(x,y)(2)P(a)(3)～Q(y)∨～R(a,y)(1)和(2),代换{a/x}(4)Q(b)(5)～R(a,b)(3)和(4),代换{b/y}(6)～S(z)∨R(a,z)(7)～S(b)(5)和(6),代换{b/z}(8)S(b)(9)□证毕■1/8/202478计算机科学与工程学院然后，在此根底上利用代换进行消解的过程如下：(1)～P(x)∨～Q(y)∨～R(x,y)(2)P(a)(3)～Q(y)∨～R(a,y)(1)和(2),代换{a/x}(4)Q(b)(5)～R(a,b)(3)和(4),代换{b/y}(6)～S(z)∨R(a,z)(7)～S(b)(5)和(6),代换{b/z}(8)S(b)(9)□证毕■1/8/202479计算机科学与工程学院然后，在此根底上利用代换进行消解的过程如下：(1)～P(x)∨～Q(y)∨～R(x,y)(2)P(a)(3)～Q(y)∨～R(a,y)(1)和(2),代换{a/x}(4)Q(b)(5)～R(a,b)(3)和(4),代换{b/y}(6)～S(z)∨R(a,z)(7)～S(b)(5)和(6),代换{b/z}(8)S(b)(9)□证毕■〔(7)和〔8〕〕1/8/202480计算机科学与工程学院

小结：谓词演算的综合推理方法一、根本推理方法1、直接证明方法2、间接证明方法〔反证法〕3、利用CP规那么二、推理中需注意的几个问题1〕当所要求的结论可能被定量时，此时可引用规那么UG和规那么EG将其量词参加。2〕在推导过程中，如既要使用规那么US又要使用规那么ES消去公式中的量词(要先使用规那么ES，再使用规那么US)。然后再使用命题演算中的推理规那么，最后使用规那么UG或规那么EG引入量词，得到所要的结论。1/8/202481计算机科学与工程学院3〕如一个变量是用规那么ES消去量词,对该变量在添加量词时,那么只能使用规那么EG,而不能使用规那么UG;如使用规那么US消去量词,对该变量在添加量词时,那么可使用规那么EG和规那么UG。4〕如有两个含有存在量词的公式，当用规那么ES消去量词时，不能选用同样的一个常量符号来取代两个公式中的变元，而应用不同的常量符号来取代它们。1/8/202482计算机科学与工程学院5〕在用规那么US和规那么ES消去量词时，此量词必须位于整个公式的最前端，并且它的辖域为其后的整个公式。6〕在添加量词(x)、(x)时，所选用的x不能在公式G(c)或G(y)中以任何约束出现。7)在使用EG规那么引入存在量词(x)，此x不得为G(c)或G(y)中的函数变元。在使用UG规那么引入全称量词(x)时，此x不得为G(y)中的函数变元(因该函数变元不得作为自由变元)。1/8/202483计算机科学与工程学院例5-6将以下三条自然公理翻译成谓词公式：每个自然数有且仅有一个直接后继；没有任何自然数以0为其直接后继；对0以外的任何自然数，有且仅有一个直接先行。解：设个体域D为自然数令p(x):x的直接先行;s(x):x的直接后继;EQUAL(x,y):x=y(x)(y)[EQUAL(y,s(x))∧(z)[EQUAL(z,s(x))→EQUAL(y,z)]]

有且仅有1/8/202484计算机科学与工程学院

～(

x)[EQUAL(0,s(x))(x)[～EQUAL(x,0)→(

y)[EQUAL(y,p(x))∧(z)[EQUAL(z,p(x))→EQUAL(y,z)]]]0以外的任何自然数1/8/202485计算机科学与工程学院例5-7解：设H(x)：x是人； M(x)：x是要死的； s：苏格拉底。那么符号化为： (x)(H(x)M(x))，H(s)M(s)证明：“所有的人都是要死的；苏格拉底是人。所以苏格拉底是要死的。〞证明：(1)(x)(H(x)M(x)) P (2)H(x)M(x) US,(1) (3)H(s) P (4)M(s) T,(2),(3)，I证明：(1)(x)(H(x)M(x)) P (2)H(s)M(s) US,(1) (3)H(s) P (4)M(s) T,(2),(3)，I(2)错了！正确的为？1/8/202486计算机科学与工程学院例5-8证明： (x)(P(x)Q(x))，(

x)P(x)(

x)Q(x)请看推导：(1)(x)(P(x)Q(x)) P(2)(P(c)Q(c)) US,(1)(3)(

x)P(x) P(4)P(c) ES,(3)(5)Q(c) T,(2),(4),I(6)(

x)Q(x) EG,(5)推导错了！应先用ES规那么，再用US规那么，正确的为？正确地推导如下：(1)(

x)P(x) P(2)P(c) ES，(1)(3)(x)(P(x)Q(x)) P(4)(P(c)Q(c)) US,(3)(5)Q(c) T,(2),(4),I(6)(

x)Q(x) EG,(5)1/8/202487计算机科学与工程学院例5-9证明：1)(

x)(P(x)∧Q(x)) P 2)(P(c)∧Q(c)) ES,1) 3)P(c) T,2),I 4)Q(c) T,2),I 5)(

x)P(x) EG,3) 6)(

x)Q(x) EG,4) 7)(

x)P(x)∧(

x)Q(x) T,5),6),I证明：(

x)(P(x)∧Q(x))(

x)P(x)∧(

x)Q(x)1/8/202488计算机科学与工程学院例5-9(续1)1)(

x)P(x)∧(

x)Q(x) P2)(

x)P(x) T,1),I3)P(c) ES,2)4)(

x)Q(x) T,1),I5)Q(c) ES,4)6)(P(c)∧Q(c)) T,3),4),I(

x)(P(x)∧Q(x)) EG,6)

请看上述推论的逆推导：推导错了！选用了同样的一个常量符号来取代两个公式中的变元，正确的为：正确的推导如下：1)(

x)P(x)∧(

x)Q(x) P2)(

x)P(x) T,1),I3)P(c) ES,2)4)(

x)Q(x) T,1),I5)Q(b) ES,4)6)(P(c)∧Q(b)) T,3),4),I7)(

x)(

y)(P(x)∧Q(y)) EG,6)这是错误的结论1/8/202489计算机科学与工程学院例5-10证明下述论断的正确性： 所有的哺乳动物都是脊椎动物； 并非所有的哺乳动物都是胎生动物； 故有些脊椎动物不是胎生的。证明设谓词如下： P(x)：x是哺乳动物； Q(x)：x是脊椎动物； R(x)：x是胎生动物。那么有：(x)(P(x)Q(x)),～(x)(P(x)R(x)) (x)(Q(x)∧～R(x))1/8/202490计算机科学与工程学院请看下面推导：～(x)(P(x)R(x)) P～(P(x)R(x)) US,1)～(～

P(x)∨R(x)) T,2)，E(P(x)∧～

R(x)) T,3),EP(x) T,4),I～R(x) T,4),I(x)(P(x)Q(x)) PP(x)Q(x) US,7)Q(x) T,(5),(8),IQ(x)∧～R(x) T,6),9),I(

x)(Q(x)∧～R(x)) EG,10)(x)(Q(x)∧～R(x)) UG,10)2〕错了！在用规那么US和规那么ES消去量词时，此量词必须位于整个公式的最前端，并且它的辖域为其后的整个公式。正确的为：1/8/202491计算机科学与工程学院证明：～(x)(P(x)R(x)) P(

x)～(～P(x)∨R(x)) T,1),E～(～P(c)∨R(c)) ES,2)(P(c)∧～R(c)) T,3),EP(c) T,4),I～R(c) T,4),I(x)(P(x)Q(x)) PP(c)Q(c) US,7)Q(c) T,5),8),IQ(c)∧～R(c) T,6),9),I(

x)(Q(x)∧～R(x)) EG,10)1/8/202492计算机科学与工程学院例5-11

证明下述论断的正确性：每个报考研究生的大学毕业生要么参加研究生的入学考试，要么被推荐为免试生；每个报考研究生的大学毕业生当且仅当学习成绩优秀才被推荐为免试生；有些报考研究生的大学毕业生学习成绩优秀，但并非所有报考研究生的大学毕业生学习成绩都优秀。因此，有些报考研究生的大学毕业生要参加研究生的入学考试。1/8/202493计算机科学与工程学院例5-11(续1)解：设P(x)：x是报考研究生的大学毕业生； Q(x)：x参加研究生入学考试； R(x)：x被推荐为免试生； S(x)：x学习成绩优秀。那么原论断可符号化为： (x)(P(x)→(Q(x)R(x))， (x)(P(x)→(R(x)S(x)))， (x)(P(x)∧S(x)), ～(x)(P(x)→S(x)) (x)(P(x)∧Q(x))1/8/202494计算机科学与工程学院例5-11(续2)证明：(1)～(x)(P(x)→S(x))P (2)(x)(P(x)∧～S(x))T,(1),E (3)P(c)∧～S(c)ES,(2) (4)P(c)T,(3),I (5)(x)(P(x)→(Q(x)R(x))P (6)P(c)→〔Q(c)R(c)〕US,(5) (7)Q(c)R(c)T,(4),(6),I (8)(x)(P(x)→(R(x)S(x)))P (9)P(c)→(R(c)S(c))US，〔8〕 (10)R(c)S(c)T,(4),(9),I1/8/202495计算机科学与工程学院例5-11(续2)证明：(1)～(x)(P(x)→S(x))P (2)(x)(P(x)∧～S(x))T,(1),E (3)P(c)∧～S(c)ES,(2) (4)P(c)T,(3),I (5)(x)(P(x)→(Q(x)R(x))P (6)P(c)→〔Q(c)R(c)〕US,(5) (7)Q(c)R(c)T,(4),(6),I (8)(x)(P(x)→(R(x)S(x)))P (9)P(c)→(R(c)S(c))US，〔8〕 (10)R(c)S(c)T,(4),(9),I1/8/202496计算机科学与工程学院例5-11(续2)证明：(1)～(x)(P(x)→S(x))P (2)(x)(P(x)∧～S(x))T,(1),E (3)P(c)∧～S(c)ES,(2) (4)P(c)T,(3),I (5)(x)(P(x)→(Q(x)R(x))P (6)P(c)→〔Q(c)R(c)〕US,(5) (7)Q(c)R(c)T,(4),(6),I (8)(x)(P(x)→(R(x)S(x)))P (9)P(c)→(R(c)S(c))US，〔8〕 (10)R(c)S(c)T,(4),(9),I1/8/202497计算机科学与工程学院例5-11(续3)(11)(R(c)→S(c))∧(S(c)→R(c))T,(10),E(12)R(c)→S(c)T,(12),I(13)～S(c)T,(3),I(14)～R(c)T,(12),(13),I(15)Q(c)T,(7),(14),I(16)P(c)∧Q(c)T,(4),(15),I(17)(

x)(P(x)∧Q(x))ES,(16)1/8/202498计算机科学与工程学院例5-11(续3)(11)(R(c)→S(c))∧(S(c)→R(c))T,(10),E(12)R(c)→S(c)T,(12),I(13)～S(c)T,(