归结推理方法.ppt

1、1,第三章 归结推理方法,概述 命题逻辑的归结法 谓词归结子句形 归结原理 归结过程的策略控制 Herbrand定理,2,3,第三章 归结推理方法,概述 命题逻辑的归结法 谓词归结子句形 归结原理 归结过程的策略控制,4,概述,归结原理由J.A.Robinson由1965年提出。 与演绎法(deductive inference)完全不同, 新的逻辑演算(inductive inference)算法。 一阶逻辑中, 至今为止的最有效的半可判定的算法。即, 一阶逻辑中任意恒真公式, 使用归结原理, 总可以在有限步内给以判定。 语义网络、框架表示、产生式规则等等都是以推理方法为前提的。即, 有了规

2、则已知条件, 顺藤摸瓜找到结果。 而归结方法是自动推理、自动推导证明用的。(“数学定理机器证明”) 本课程只讨论一阶谓词逻辑描述下的归结推理方法, 不涉及高阶谓词逻辑问题。,5,第三章 归结推理方法,概述 命题逻辑的归结法 谓词归结子句形 归结原理 归结过程的策略控制 Herbrand定理,6,第三章 归结推理方法,概述 命题逻辑的归结法 谓词归结子句形 归结原理 归结过程的策略控制 Herbrand定理,7,命题例,命题： 能判断真假(不是既真又假)的陈述句。 简单陈述句描述事实、事物的状态、关系等性质。 例如：1. 1+1=2 2. 雪是黑色的。 3. 北京是中国的首都。 4. 我到冥王星

3、去渡假。,8,命题例,判断一个句子是否是命题, 有先要看它是否是陈述句, 而后看它的真值是否唯一。以上的例子都是陈述句, 第4句的真值现在是假, 随着人类科学的发展, 有可能变成真, 但不管怎样, 真值是唯一的。因此, 以上4个例子都是命题。 而例如：1. 快点走吧！ 2. 到那去？ 3. x+y10 等等句子, 都不是命题。,9,命题逻辑的归结法,命题逻辑基础： 定义： 合取式：p与q, 记做p q 析取式： p或q, 记做p q 蕴含式： 如果p则q, 记做p q 等价式：p当且仅当q, 记做p q 。,10,命题表示公式(1),将陈述句转化成命题公式。 如：设“下雨”为p, “骑车上班”

4、为q, 1.“只要不下雨, 我骑自行车上班”。 p 是 q的充分条件, 因而, 可得命题公式： p q 2.“只有不下雨, 我才骑自行车上班”。 p 是 q的必要条件, 因而, 可得命题公式：q p,11,命题表示公式(2),例如： 1. “如果我进城我就去看你, 除非我很累。” 设：p, 我进城, q, 去看你, r, 我很累。 则有命题公式： r (p q)。 2. “应届高中生, 得过数学或物理竞赛的一等 奖, 保送上北京大学。” 设：p, 应届高中生, q, 保送上北京大学上学, r, 是得过数学一等奖。t, 是得过物理一等奖。 则有命题公式公式：p (r t ) q。,12,命题逻辑

5、基础,定义： 若A无成假赋值, 则称A为重言式或永真式； 若A无成真赋值, 则称A为矛盾式或永假式； 若A至少有一个成真赋值, 则称A为可满足的； 析取范式：仅由有限个简单合取式组成的析取式。 合取范式：仅由有限个简单析取式组成的合取式。,13,命题逻辑基础,基本等值式24个(1) 交换律：p q q p ； p q q p 结合律：(pq) r p(q r); (p q) r p (q r) 分配律： p (q r) (p q) (p r) ； p (q r) (p q) (p r),14,命题逻辑基础,基本等值式(1) 摩根律: (pq) p q ； (p q) p q 吸收律: p (p

6、 q ) p ； p (p q ) p 同一律: p 0 p ； p 1 p 蕴含等值式:p q p q 假言易位式: p q p q,15,推理定律,推理定律重言蕴涵式 重要的推理定律 A (AB) 附加律 (AB) A 化简律 (AB)A B 假言推理 (AB)B A 拒取式,16,推理定律,(AB)B A 析取三段论 (AB)(BC) (AC) 假言三段论 (AB)(BC) (AC) 等价三段论 (AB)(CD)(AC) (BD) 构造性二难 (AB)(AB)(AA) B 构造性二难(特殊形式) (AB)(CD)( BD) (AC) 破坏性二难,17,在自然推理系统P中构造证明 1. 直

7、接证明法 例 用构造证明法构造下面推理的证明: 若明天是星期一或星期三, 我就有课. 若有课, 今天必备课. 我今天下午没备课. 所以, 说明天是星期一或星期三是不对的. 构造证明 设p: 明天是星期一, q: 明天是星期三, r: 我有课, s: 我备课 形式结构 前提: (pq)r, rs, s 结论: pq,18,证明 rs 前提引入 s 前提引入 r 拒取式 (pq)r 前提引入 (pq) 拒取式 pq 置换,19,2. 附加前提证明法 (1)欲证: 前提: A1, A2, , Ak 结论: CB (2)等价地证明 前提: A1, A2, , Ak, C 结论: B (3)理由: (A

8、1A2Ak)(CB) ( A1A2Ak)(CB) ( A1A2AkC)B (A1A2AkC)B,20,例: 构造下面推理的证明 2是素数或合数. 若2是素数, 则21/2是无理数. 若21/2是无理数, 则4不是素数. 所以, 如果4是素数, 则2是合数. 用附加前提证明法构造证明 (1)设p: 2是素数, q: 2是合数, r: 21/2是无理数, s: 4是素数 (2)形式结构 前提: pq, pr, rs 结论: sq,21,(3)证明 s 附加前提引入 pr 前提引入 rs 前提引入 ps 假言三段论 p 拒取式 pq 前提引入 q 析取三段论,22,3. 归谬法(或称反证法) (1)

9、欲证 A1A2AkB 前提: A1, A2, , Ak 结论: B (2)将B当前提, 推出矛盾, 得证(1)正确 (3)理由 A1A2AkB (A1A2Ak)B (A1A2AkB) 括号内部为矛盾式当且仅当 (A1A2AkB)为重言式,23,例: 前提: (pq)r, rs, s, p 结论: q 证明(用归缪法) q 结论否定引入 rs 前提引入 s 前提引入 r 拒取式 (pq)r 前提引入 (pq) 析取三段论 pq 置换 p 析取三段论 p 前提引入 pp 合取,24,命题逻辑的归结法,基本单元：简单命题(陈述句) 例： 命题： A1、A2、A3 和 B 求证： A1A2 A3成立,

10、 则B成立, 即：A1 A2 A3 B 反证法：证明A1 A2 A3 B 是矛盾式 (永假式),25,命题逻辑的归结法,建立子句集 合取范式：命题、命题或的与, 如： P(PQ)(PQ) 子句集S：合取范式形式下的子命题(元素)的集合 例：命题公式：P(PQ)(PQ) 子句集 S：S = P, PQ, PQ,26,命题逻辑的归结法,归结式 消除互补文字对, 求新子句得到归结式。 如子句： C1 =C1L, C2=C2L, 归结式：R(C1, C2) = C1C2 注意：C1 C2 R(C1, C2) , 反之不一定成立。,27,命题逻辑的归结法,归结过程 将命题写成合取范式 求出子句集 对子句

11、集使用归结推理规则 归结式作为新子句参加归结 归结式为空子句 , S是不可满足的(矛盾), 原命题成立。 (证明完毕) 谓词的归结：除了有量词和函数以外, 其余和命题归结过程一样。,28,命题逻辑归结例题(1),例题, 证明公式：(P Q) (Q P) 证明： (1)根据归结原理, 将待证明公式转化成待归结命题公式： (P Q) (Q P) (2)分别将公式前项化为合取范式： P Q P Q 结论求后的后项化为合取范式： (Q P) (QP) Q P 两项合并后化为合取范式： (P Q)Q P (3)则子句集为： PQ, Q, P,29,命题逻辑归结例题(2),子句集为： PQ, Q, P (

12、4)对子句集中的子句进行归结可得： 1. PQ 2. Q 3. P 4. Q, (1, 3归结) 5. , (2, 4归结) 由上可得原公式成立。,30,第三章 归结推理方法,概述 命题逻辑的归结法 谓词归结子句形 归结原理 归结过程的策略控制 Herbrand定理,31,第三章 归结推理方法,概述 命题逻辑的归结法 谓词归结子句形 归结原理 归结过程的策略控制 Herbrand定理,32,谓词归结原理基础,一阶逻辑 基本概念 个体词：表示主语的词 谓词：刻画个体性质或个体之间关系的词 量词：表示数量的词,33,谓词归结原理基础,小王是个工程师。 8是个自然数。 我去买花。 小丽和小华是朋友。

13、 其中, “小王”、“工程师”、“我”、“花”、“8”、“小丽”、“小华”都是个体词, 而“是个工程师”、“是个自然数”、“去买”、“是朋友”都是谓词。显然前两个谓词表示的是事物的性质, 第三个谓词“去买”表示的一个动作也表示了主、宾两个个体词的关系, 最后一个谓词“是朋友”表示两个个体词之间的关系。,34,谓词归结原理基础,一阶逻辑 公式及其解释 个体常量：a, b, c 个体变量：x, y, z 谓词符号：P, Q, R 量词符号： , ,35,谓词归结原理基础,例如：(1)所有的人都是要死的。 (2) 有的人活到一百岁以上。 在个体域D为人类集合时, 可符号化为： (1)xP(x), 其

14、中P(x)表示x是要死的。 (2)xQ(x), 其中Q(x)表示x活到一百岁以上。 在个体域D是全总个体域时, 引入特殊谓词R(x)表示x是人, 可符号化为： (1)x(R(x) P(x), 其中, R(x)表示x是人；P(x)表示x是要死的。 (2)x(R(x) Q(x), 其中, R(x)表示x是人；Q(x)表示x活到一百岁以上。,36,谓词归结原理基础,量词否定等值式： ( x ) M(x) ( y ) M(y) ( x ) M(x) ( y ) M(y) 量词分配等值式： ( x )(P(x) Q(x) ( x ) P(x) ( x ) Q(x) ( x )(P(x) Q(x) ( x

15、 ) P(x) ( x ) Q(x) 消去量词等值式：设个体域为有穷集合(a1, a2, an) (x ) P(x) P(a1 ) P(a2 ) P(an ) ( x )P(x) P(a1 ) P(a2 ) P(an ),37,一阶(first order)逻辑的合式公式,项 原子公式 合式公式,38,项(term),个体常项和个体变项是项 若(x1, x2, , xn)是n元函数, t1, t2, , tn是项, 则(t1, t2, , tn)是项 所有的项都是有限次地应用上述规则形成的 例如: a, x, f(a), g(a, x), g(x, f(a),39,原子公式(atomic fo

16、rmula),若R(x1, x2, , xn)是n元谓词, t1, t2, , tn是项, 则R(t1, t2, , tn)是原子公式 例如: F(a), G(a, y), F(f(a), G(x, g(a, y),40,合式公式(well-formed formula),原子公式是合式公式 若A是合式公式, 则(A)是合式公式 若A, B是合式公式, 则(AB), (AB), (AB), (AB)也是合式公式 若A是合式公式, 则xA, xA也是合式公式 只有有限次地应用上述规则形成的符号串才是合式公式,41,合式公式(举例),x(F(x)y(G(y)H(x, y) F(f(a, a), b

17、) 约定：省略多余括号 最外层 优先级递减： , ; ; , ; , ,42,合式公式中的变项,量词辖域: 在xA, xA中, A是量词的辖域. 例如: x(F(x)y(G(y)H(x, y) 指导变项: 紧跟在量词后面的个体变项.例如: x(F(x)y(G(y)H(x, y) 约束出现: 在辖域中与指导变项同名的变项. 例如: x(F(x)y(G(y)H(x, y) 自由出现: 既非指导变项又非约束出现. 例如: y(G(y)H(x, y),43,合式公式中的变项(举例),H(x, y)xF(x)y(G(y)H(x, y) x与 y是指导变项 x与y是约束出现 x与 y是自由出现,44,换名

18、(rename)规则,把某个指导变项和其量词辖域中所有同名的约束出现, 都换成某个新的个体变项符号. 例如: x(A(x)B(x) y(A(y)B(y) xA(x)xB(x) yA(y)zB(z) H(x, y)xF(x)y(G(y)H(x, y) H(x, y)zF(z)u(G(u)H(x, u),45,代替(substitute)规则,把某个自由变项的所有出现, 都换成某个新的个体变项符号. 例如: A(x)B(x) A(y)B(y) xA(x)B(x) xA(x)B(y) H(x, y)xF(x)y(G(y)H(x, y) H(s, t)xF(x)y(G(y)H(s, y),46,解释(

19、interpret),对一个合式公式的解释包括给出 个体域 谓词 函数 个体常项 的具体含义,47,解释(举例),F(f(a, a), b) 解释1： 个体域是全体自然数; a: 2; b: 4; f(x, y)=x+y; F(x, y): x=y 原公式解释成: “2+2=4”。 解释2： 个体域是全体实数; a: 3; b: 5; f(x, y)=x-y; F(x, y): xy 原公式解释成: “3-35”。,48,谓词归结原理基础,量词分配等值式 x(A(x)B(x) xA(x)xB(x) x(A(x)B(x) xA(x)xB(x) 注意: 对无分配律, 对无分配律,49,量词分配(反

20、例),x(A(x)B(x) xA(x)xB(x) x(A(x)B(x) xA(x)xB(x) 个体域为全体自然数; A(x): x是偶数 B(x): x是奇数; 左1, 右0 x(A(x)B(x) xA(x)xB(x) x(A(x)B(x) xA(x)xB(x) 个体域为全体自然数; A(x): x是偶数 B(x): x是奇数; 左0, 右1,50,谓词归结原理基础,量词辖域收缩与扩张等值式： ( x )(P(x) Q) ( x ) P(x) Q ( x )(P(x) Q) ( x ) P(x) Q ( x )(P(x) Q) ( x ) P(x) Q ( x )(Q P(x) ) Q ( x

21、 ) P(x) ( x )(P(x) Q) ( x ) P(x) Q ( x )(P(x) Q) ( x ) P(x) Q ( x )(P(x) Q) ( x ) P(x) Q ( x )(Q P(x) ) Q ( x ) P(x),51,前束范式,前束范式与公式的前束范式 1. 前束范式 定义 设A为一个一阶逻辑公式, 若A具有如下形式 Q1x1Q2x2QkxkB 则称A为前束范式, 其中Qi (1 i k)为或, B为不含量词的公式. 例如, x(F(x)y(G(y)H(x, y) 不是前束范式, xy(F(x)(G(y)H(x, y) 是前束范式. 又如, x(F(x)G(x) 不是前束

22、范式, x(F(x)G(x) 是前束范式.,52,2. 公式的前束范式 定理 (前束范式存在定理)一阶逻辑中的任何公式都存在与之等值的前束范式(不惟一) 3. 如何求公式的前束范式 利用重要等值式、置换规则、换名规则、代替规则进行等值演算,53,例 求下列公式的前束范式 (1)x(M(x)F(x) (2)xF(x)xG(x) (3)xF(x)xG(x) (4)xF(x)y(G(x, y)H(y) (5)x(F(x, y)y(G(x, y)H(x, z) 解 (1)x(M(x)F(x) x(M(x)F(x) (量词否定等值式) x(M(x)F(x) 两步结果都是前束范式, 说明不惟一性.,54,

23、(2)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) 两种形式是等值的,55,(3)xF(x)xG(x) xF(x)xG(x) x(F(x)G(x) (为什么？) 或 xy(F(x)G(y) (为什么？),56,(4)xF(x)y(G(x, y)H(y) zF(z)y(G(x, y)H(y) (换名规则) zy(F(z)(G(x, y)H(y) (为什么?) 或 xF(x)y(G(z, y)H(y) (代替规则) xy(F(x)(G(

24、z, y)H(y),57,(5)可用换名规则, 也可用代替规则, 这里用代替规则 x(F(x, y)y(G(x, y)H(x, z) x(F(x, u)y(G(x, y)H(x, z) xy(F(x, u)G(x, y)H(x, z) 注意: x与y不能颠倒,58,谓词推理(举例),前提: x(F(x)G(x), F(a) 结论: G(a) 证明: (1) F(a) 前提引入 (2) x(F(x)G(x) 前提引入 (3) F(a)G(a) (2)UI (4) G(a) (1)(3)假言推理,59,谓词归结子句形(Skolem 标准形),SKOLEM标准形 前束范式 说公式A是一个前束范式,

25、如果A中的一切量词都位于该公式的最左边(不含否定词), 且这些量词的辖域都延伸到公式的末端。,60,谓词归结子句形(Skolem 标准形),即： 把所有的量词都提到前面去, 然后消掉所有量词 (Q1x1)(Q2x2)(Qnxn)M(x1, x2, , xn) 约束变项换名规则： (Qx ) M(x) (Qy ) M(y) (Qx ) M(x, z) (Qy ) M(y, z),61,谓词归结子句形(Skolem 标准形), 量词消去原则： 消去存在量词“”, 略去全程量词“”。 注意：左边有全程量词的存在量词, 消去时该变量改写成为全程量词的函数；如没有, 改写成为常量。,62,谓词归结子句形

26、(Skolem 标准形), Skolem定理： 谓词逻辑的任意公式都可以化为与之等价的前束范式, 但其前束范式不唯一。 SKOLEM标准形定义： 消去量词后的谓词公式。 注意：谓词公式G的SKOLEM标准形同G并不等值。,63,谓词归结子句形(Skolem 标准形),例:将下式化为Skolem标准形： (x)(y)P(a, x, y) (x)(y)Q(y, b)R(x) 解：第一步, 消去号, 得： (x)(y)P(a, x,y)(x)(y)Q(y, b)R(x) 第二步, 深入到量词内部, 得： (x)(y)P(a, x, y) (x)(y)Q(y, b)R(x) (x)(y)P(a, x,

27、 y)(x)(y)(Q(y, b)R(x),64,谓词归结子句形(Skolem 标准形),第三步, 任意量词左移(分配律), 变元易名, 得 (x)(y)P(a,x,y)(z) (Q(z, b)R(x) 第四步, 存在量词左移, 直至所有的量词移到前面, 得： (x)(y)(z)P(a, x, y) Q(z, b)R(x) 由此得到前束范式,65,谓词归结子句形(Skolem 标准形),第五步, 消去“”(存在量词), 略去“”全称量词消去(y), 因为它左边只有(x), 所以使用x的函数f(x)代替之, 这样得到： (x)(z)(P(a, x, f(x) Q(z, b)R(x) 消去(z),

28、 同理使用g(x)代替之, 这样得到： (x) (P(a, x, f(x) Q(g(x), b)R(x) 则, 略去全称变量, 原式的Skolem标准形为： P(a, x, f(x) Q(g(x), b)R(x),66,谓词归结子句形,子句与子句集 文字：不含任何连接词的谓词公式。 子句：一些文字的析取(谓词的和)。 子句集S的求取： G SKOLEM标准形 消去存在变量 以“, ”取代“”, 并表示为集合形式 。,67,谓词归结子句形,G是不可满足的S是不可满足的 G与S不等价, 但在不可满足得意义下是一致的。 定理： 若G是给定的公式, 而S是相应的子句集, 则G是不可满足的S是不可满足的

29、。 注意：G真不一定S真, 而S真必有G真。 即： S G,68,谓词归结子句形,G = G1 G2 G3 Gn 的子句形 G的字句集可以分解成几个单独处理。 有 SG = S1 U S2 U S3 U U Sn 则SG 与 S1 U S2 U S3 U U Sn在不可满足得意义上是一致的。 即SG 不可满足S1 U S2 U S3 U U Sn不可满足,69,求取子句集例(1),例：对所有的x, y, z来说, 如果y是x的父亲, z又是y的父亲, 则z是x的祖父。又知每个人都有父亲, 试问对某个人来说谁是它的祖父？ 求：用一阶逻辑表示这个问题, 并建立子句集。 解：这里我们首先引入谓词：

30、P(x, y) 表示x是y的父亲 Q(x, y) 表示x是y的祖父 ANS(x) 表示问题的解答,70,求取子句集例(2),对于第一个条件, “如果x是y 的父亲, y又是z 的父亲, 则x是z 的祖父”, 一阶逻辑表达式如下： A1：(x)(y)(z)(P(x, y)P(y, z)Q(x, z) SA1：P(x , y)P(y, z)Q(x, z) 对于第二个条件：“每个人都有父亲”, 一阶逻辑表达式： A2：(y)(x)P(x, y) SA2：P(f(y), y),71,求取子句集例(2),对于结论：某个人是它的祖父 B：(x)(y)Q(x, y) 否定后得到子句： (x)(y)Q(x,

31、y) ANS(x) SB：Q(x, y)ANS(x) 则得到的相应的子句集为： SA1, SA2, SB ,72,第三章 归结推理方法,概述 命题逻辑的归结法 谓词归结子句形 归结原理 归结过程的策略控制 Herbrand定理,73,第三章 归结推理方法,概述 命题逻辑的归结法 谓词归结子句形 归结原理 归结过程的策略控制 Herbrand定理,74,归结原理,归结原理正确性的根本在于, 找到矛盾可以肯定不真。 方法： 和命题逻辑一样。 但由于有函数, 所以要考虑合一和置换。,75,置换,置换： 可以简单的理解为是在一个谓词公式中用置换项去置换变量。 定义： 置换是形如t1/x1, t2/x2

32、, , tn/xn的有限集合。其中, x1, x2, , xn是互不相同的变量, t1, t2, , tn是不同于xi的项(常量、变量、函数)；ti/xi表示用ti置换xi, 并且要求ti与xi不能相同, 而且xi不能循环地出现在另一个ti中。 例如 a/x, c/y, f(b)/z是一个置换。 g(y)/x, f(x)/y不是一个置换,76,置换的合成,设t1/x1, t2/x2, , tn/xn, u1/y1, u2/y2, , un/yn, 是两个置换。 则与的合成也是一个置换, 记作。它是从集合 t1/x1, t2/x2, , tn/xn, u1/y1, u2/y2, , un/yn

33、中删去以下两种元素： 当ti =xi时, 删去ti /xi (i = 1, 2, , n); 当yix1, x2, , xn时, 删去uj/yj (j = 1, 2, , m) 最后剩下的元素所构成的集合。 合成即是对ti先做置换然后再做置换, 置换xi,77,置换的合成,例： 设：f(y)/x, z/y, a/x, b/y, y/z, 求与的合成。 解：先求出集合 f(b/y)/x, (y/z)/y, a/x, b/y, y/zf(b)/x, y/y, a/x, b/y, y/z 其中, f(b)/x中的f(b)是置换作用于f(y)的结果；y/y中的y是置换作用于z的结果。在该集合中, y/

34、y满足定义中的条件i, 需要删除；a/x, b/y满足定义中的条件ii, 也需要删除。最后得 f(b)/x, y/z,78,合一,合一可以简单地理解为“寻找相对变量的置换, 使两个谓词公式一致”。 定义：设有公式集FF1, F2, , Fn, 若存在一个置换, 可使F1F2= Fn, 则称是F的一个合一。同时称F1, F2, . , Fn是可合一的。 例： 设有公式集FP(x, y, f(y), P(a, g(x), z), 则a/x, g(a)/y, f(g(a)/z是它的一个合一。 注意：一般说来, 一个公式集的合一不是唯一的。,79,归结原理,归结的注意事项： 谓词的一致性, P()与Q

35、(), 不可以 常量的一致性, P(a, )与P(b, .), 不可以 变量, P(a, .)与P(x, ), 可以 变量与函数, P(a, x, .)与P(x, f(x), ), 不可以； 是不能同时消去两个互补对, PQ与PQ的空, 不可以 先进行内部简化(置换、合并),80,归结原理,归结的过程 写出谓词关系公式 用反演法写出谓词表达式 SKOLEM标准形 子句集S 对S中可归结的子句做归结 归结式仍放入S中, 反复归结过程 得到空子句 命题得证,81,例题“快乐学生”问题,假设任何通过计算机考试并获奖的人都是快乐的, 任何肯学习或幸运的人都可以通过所有的考试, 张不肯学习但他是幸运的,

36、 任何幸运的人都能获奖。求证：张是快乐的。 解：先将问题用谓词表示如下： R1:“任何通过计算机考试并获奖的人都是快乐的” (x)(Pass(x, computer)Win(x, prize)Happy(x),82,例题“快乐学生”问题,R2:“任何肯学习或幸运的人都可以通过所有考试” (x)(y)(Study(x)Lucky(x)Pass(x, y) R3:“张不肯学习但他是幸运的” Study(zhang)Lucky(zhang) R4:“任何幸运的人都能获奖” (x)(Lucky(x)Win(x, prize) 结论：“张是快乐的”的否定 Happy(zhang),83,例题“快乐学生”

37、问题,由R1及逻辑转换公式:PWH = (PW) H , 可得 (1)Pass(x, computer)Win(x, prize)Happy(x) 由R2(变量更名处理)： (2)Study(y)Pass(y, z) (3)Lucky(u)Pass(u, v) 由R3： (4)Study(zhang) (5)Lucky(zhang) 由R4 (变量更名处理) ： (6)Lucky(w)Win(w, prize) 由结论(否定)： (7)Happy(zhang)(结论的否定),84,例题“快乐学生”问题,(8)Pass(w, computer)Happy(w)Luck(w) (1)(6), w/

38、x (9)Pass(zhang, computer)Lucky(zhang) (8)(7), zhang/w (10)Pass(zhang, computer) (9)(5) (11)Lucky(zhang) (10)(3), zhang/u, computer/v (12) (11)(5),85,归结原理,归结法的实质： 归结法是仅有一条推理规则的推理方法。 归结的过程是一个语义树倒塌的过程。 归结法的问题 子句中有等号或不等号时, 完备性不成立。 Herbrand定理的不实用性引出了可实用的归结法。,86,第三章 归结推理方法,概述 命题逻辑的归结法 谓词归结子句形 归结原理 归结过程的策

39、略控制 Herbrand定理,87,第三章 归结推理方法,概述 命题逻辑的归结法 谓词归结子句形 归结原理 归结过程的策略控制 Herbrand定理,88,归结过程的控制策略,要解决的问题： 归结方法的知识爆炸。 控制策略的目的 归结点尽量少 控制策略的原则 给出控制策略, 以使仅对选择合适的子句间方可做归结。避免多余的、不必要的归结式出现。或者说, 少做些归结仍能导出空子句。,89,例:SPQ,PQ，PQ,PQ 来证明是不满足的。证明过程是从S0S 出发。依次构造Si=C1, C2的归结式C1S0S1Si-1, C2Si-1 i=1,2,直至出现空子句证明结束。这就是盲目全面归结的描述。具体

40、的归结过程是 S0 (1)P Q (2) PQ (3)P Q (4)PQS1 (5)Q (1)(2) (6)P (1)(3) (7)QQ (1)(4) (8)PP (1)(4) (9)Q Q (2)(3) (10) PP (2)(3) (11)P (2)(4) (12)Q (3)(4),90,S2 (13)P Q (1)(7) (14) P Q (1)(8) (15)P Q (1)(9) (16)P Q (1)(10) (17)Q (1)(11) (18)P (1)(12) (19)Q (2)(6) (20)P Q (2)(7) (21) P Q (2)(8) (22)P Q (2)(9) (

41、23)P Q (2)(10)(24)P (2)(12) (25)P (3)(5) (26)PQ (3)(7) (27)P Q (3)(8) (28)P Q (3)(9) (29)PQ(3)(10) (30)Q (3)(11) (31)P (4)(5) (32)Q (4)(6) (33)PQ (4)(7)(34)P Q (4)(8) (35)P Q (4)(9) (36)P Q (4)(10) (37) Q (5)(7) (38)Q (5)(9) (39) (5)(12),91,在这种归结过程中产生了相当数量的不必要的归结式。一类是重言式如(7)(10)，由它们又产生了归结式(13)(16)，(

42、20)(23)，(26)(29)，(33)(39)。另一类是重复的，如P,Q,P,Q就多次出现过。就这个例子而言，若由人来证明只需三步，(5)(12)(39)便得空子句，这节将介绍删除策略、语义归结和线性归结等控制策略。,92,控制策略的方法(1),删除策略完备 名词解释：归类：设有两个子句C和D, 若有置换使得C D成立, 则称子句C把子句D归类。 由于小的可以代表大的, 所以小的吃掉大的了。 若对S使用归结推理过程中, 当归结式Cj是重言式(永真式)和Cj被S中子句和子句集的归结式Ci(ij)所归类时, 便将Cj删除。这样的推理过程便称做使用了删除策略的归结过程。,93,控制策略的方法(1

43、),主要思想：归结过程在寻找可归结子句时, 子句集中的子句越多, 需要付出的代价就会越大。如果在归结时能把子句集中无用的子句删除掉, 就会缩小搜索范围, 减少比较次数, 从而提高归结效率。删除策略对阻止不必要的归结式的产生来缩短归结过程是有效的。然而要在归结式Cj产生后方能判别它是否可被删除, 这部分计算量是要花费的, 只是节省了被删除的子句又生成的归结式。尽管使用删除策略的归结, 少做了归结但不影响产生空子句, 就是说删除策略的归结推理是完备的。,94,控制策略的方法(2),采用支撑集完备 支撑集：设有不可满足子句集S的子集T, 如果S-T是可满足的, 则T是支持集。 采用支撑集策略时, 从

44、开始到得到的整个归结过程中, 只选取不同时属于S-T的子句, 在其间进行归结。就是说, 至少有一个子句来自于支撑集T或由T导出的归结式。,95,例如：A1A2 A3 B中的B可以作为支撑集使用。要求每一次参加归结的亲本子句中, 只要应该有一个是有目标公式的否定(B)所得到的子句或者它们的后裔。 支撑集策略的归结是完备的, 同样, 所有可归结的谓词公式都可以用采用支撑集策略达到加快归结速度的目的。问题是如何寻找合适的支撑集。一个最容易找到的支撑集是目标子句的非, 即SB。,96,例:SPQ,PR,QR，R取TR支持集归结过程(1) PQ(2) PR(3) QR(4) R(5) P (2)(4)(

45、6) Q (3)(4)(7) Q (1)(5)(8) P (1)(6)(9) R (3)(7)(10) (6)(7),97,98,控制策略的方法(3),语义归结完备 语义归结策略是将子句S按照一定的语义分成两部分, 约定每部分内的子句间不允许作归结。同时还引入了文字次序, 约定归结时其中的一个子句的被归结文字只能是该子句中“最大”的文字。,99,控制策略的方法(3),语义归结策略的归结是完备的, 同样, 所有可归结的谓词公式都可以用采用语义归结策略达到加快归结速度的目的。问题是如何寻找合适的语义分类方法, 并根据其含义将子句集两个部分中的子句进行排序。,100,例:SPQR, PR, QR,

46、R. 我们先规定S中出现的文字的次序，如依次为P，Q，R或记作PQR。再选取S的一个解释I，如令IP,Q,R用它来将S分成两个部分。规定在I下为假的子句放入S1中，在I下为真的子句放入S2中。于是有S1=PR,QRS2PQR,R规定S1内部的子句不允许归结，S1与S2子句间的归结必须是S 中的最大文字方可进行。这样所得的归结式，仍按I来放入S1或S2。,101,归结过程(1) PQ R S2(2) PR S1(3) QR S1(4) R S2(5) QR (2)(1)归结 S2(6) PR (3)(1)归结 S2(7) R (2)(6)归结 S1(8) R (3)(5)归结 S1(9) (7)

47、(4)归结这是采用了语义归结策略下的盲目全面归结过程。明显地减少归结次数。阻止了(1)(4)的归结，也阻止了(2)(4)的归结。,102,控制策略的方法(4),线性归结 完备 线性归结策略首先从子句集中选取一个称作顶子句的子句C0开始作归结。归结过程中所得到的归结式Ci立即同另一子句Bi进行归结得归结式Ci+1。而Bi属于S或是已出现的归结式Cj(ji)。即, 如下图所示归结得到的新子句立即参加归结。,103,104,例:SPQ ,PQ,PQ,PQ选取顶子句C0PQ。线性归结过程(1) PQ(2) PQ(3) PQ(4) PQ(5) Q (1)(2)(6) P (5)(3)(7) Q (6)(

48、4)(8) (7)(5)顶子句的选择直接影响着归结的效率。如可选得C0使SC0是可满足的。,105,控制策略的方法(4),线性归结是完备的, 同样, 所有可归结的谓词公式都可以采用线性归结策略达到加快归结速度的目的。如果能搞找到一个较好的顶子句, 可以式归结顺利进行。否则也可能事与愿违。,106,控制策略的方法(5),单元归结完备 单元归结策略要求在归结过程中, 每次归结都有一个子句是单元子句(只含一个文字的子句)或单元因子。显而易见, 词中方法可以简单地削去另一个非单子句中的一个因子, 使其长度减少, 构成简单化, 归结效率较高。 初始子句集中没有单元子句时, 单元归结策略无效。所以说“反之

49、不成立”, 即此问题不能采用单元归结策略。,107,例:SPQ ,PR,Q R,R单元归结过程(1) PQ(2) PR(3) QR(4) R(5) P (4)(2)(6) Q (4)(3)(7) Q (5)(1)(8) P (6)(1)(9) R (7)(3)(10) (7)(6),108,控制策略的方法(6),输入归结 完备 与单元归结策略相似, 输入归结策略要求在归结过程中, 每一次归结的两个子句中必须有一个是S的原始子句。这样可以避免归结出的不必要的新子句加入归结, 造成恶性循环。可以减少不必要的归结次数。,109,例:SPQ ,PR,Q R,R输入归结过程(1) PQ(2) PR(3)

50、 QR(4) R(5) QR(1)(2)(6) R (3)(5)(7) (4)(6),110,控制策略的方法(6),如同单元归结策略, 不是所有的可归结谓词公式的最后结论都是可以从原始子句集中的得到的。简单的例子, 归结结束时, 即最后一个归结式为空子句的条件是, 参加归结的双方必须是两个单元子句。原始子句集中没有单元子句的谓词公式一定不能采用输入归结策略。,111,第三章 归结推理方法,概述 命题逻辑的归结法 谓词归结子句形 归结原理 归结过程的策略控制 Herbrand定理,112,第三章 归结推理方法,概述 命题逻辑的归结法 谓词归结子句形 归结原理 归结过程的策略控制 Herbrand

51、定理,113,Herbrand定理,问题： 一阶逻辑公式的永真性(永假性)的判定是否能在有限步内完成？,114,Herbrand定理,1936年图灵(Turing)和邱吉(Church)互相独立地证明了：,“没有一般的方法使得在有限步内判定一阶逻辑的公式是否是永真(或永假)。但是如果公式本身是永真(或永假)的, 那么就能在有限步内判定它是永真(或永假)。对于非永真(或永假)的公式就不一定能在有限步内得到结论。判定的过程将可能是不停止的。”,115,Herbrand定理,Herbrand的思想 定义： 公式G永真：对于G的所有解释, G都为真。 思想： 寻找一个已给的公式是真的解释。然而, 如果

52、所给定的公式的确是永假的, 就没有这样的解释存在, 并且算法在有限步内停止。,116,Herbrand定理,H域 H解释 语义树 结论：Herbrand定理,117,Herbrand定理,H域 H解释 语义树 结论：Herbrand定理,118,Herbrand定理(H域),基本方法： 因为量词是任意的, 所讨论的个体变量域D是任意的, 所以解释的个数是无限、不可数的 。 简化讨论域。建立一个比较简单、特殊的域, 使得只要在这个论域上, 该公式是不可满足的。 此域称为H域。,119,Herbrand定理(H域),设G是已给的公式，定义在论域D上，令H0是G中所出现的常量的集合。若G中没有常量出

53、现，就任取常量aD，而规定H0=a。 Hi= Hi-1所有形如f(t1,tn)的元素 其中f(t1,tn)是出现于G中的任一函数符号，而t1,tn 是Hi-1的元素，i=1,2,。 规定H为G的H域(或说是相应的子句集S的H域)。 不难看出，H域是直接依赖于G的最多只有可数个元素。,120,121,H域例题,例1:S=P(a),P(x)P(f(x) 依定义有 H0=a H1=af(a)=a,f(a) H2=a,f(a)f(a),f(f(a)=a,f(a),f(f(a) H=a,f(a),f(f(a),122,H域例题,例2:S=P(z),P(x)Q(y) 依定义有 H0=a a是论域D中一常量

54、。 H1= H0 H2= H1 H=a,123,H域例题,例3:S=P(f(x),a,g(y),b) 依定义有 H0=a,b H1=a,b,f(a),g(a),f(b),g(b) H2=(a,b,f(a),g(a),f(b),g(b),f(f(a), f(g(a),f(f(b),f(g(b),g(f(a),g(g(a),g(f(b),g(g(b) H=H0H1H2 如果在S中出现函数形如f(x,a)仍视为f(x1, x2)的形式，这时若H0=a,b,则H1中除有f(a,a),f(b,a)外，还出现f(a,b),f(b,b)。,124,H域例题,例4:设子句集S = P(x), Q(y, f(z

55、, b), R(a), 求H域 解： H0 a, b为子句集中出现的常量 H1 a, b, f(a, b), f(a, a), f(b, a), f(b, b),125,H域例题,H2 a, b, f(a, b), f(a, a), f(b, a), f(b, b), f(a, f(a, b), f(a, f(a, a), f(a, f(b, a), f(a, f(b, b), f(b, f(a, b), f(b, f(a, a), f(b, f(b, a), f(b, f(b, b), f(f(a, b), f(a, b), f(f(a, b), f(a, a), f(f(a, b), f(

56、b, a), f(f(a, b), f(b, b), f(f(a, a), f(a, b), f(f(a, a), f(a, a), f(f(a, a), f(b, a), f(f(a, a), f(b, b), f(f(b, a), f(a, b), f(f(b, a), f(a, a), f(f(b, a), f(b, a), f(f(b, a), f(b, b), f(f(b, b), f(a, b), f(f(b, b), f(a, a), f(f(b, b), f(b, a), f(f(b, b), f(b, b) H = H1H2H3,126,Herbrand定理(H域),几个基本

57、概念 f(tn)：f为子句集S中的所有函数变量。t1, t2, , tn为S的H域的元素。通过它们来讨论永真性。 原子集A：谓词套上H域的元素组成的集合。如A = 所有形如 P(t1, t2, tn)的元素 即把H中的东西填到S的谓词里去。S中的谓词是有限的, H是可数的, 因此, A也是可数的。,127,原子集例题,上例题的原子集为： A = P(a), Q(a, a), R(a), P(b), Q(b, a), Q(b, b), Q(a, b), R(b), P(f(a, b), Q(f(a, b), f(a, b), R(f(a, b), P(f(a, a), P(f(b, a), P(

58、f(b, b), ) 一旦原子集内真值确定好(规定好), 则S在H上的真值可确定。成为可数问题。,128,Herbrand定理,H域 H解释 语义树 结论：Herbrand定理,129,Herbrand定理,H域 H解释 语义树 结论：Herbrand定理,130,Herbrand定理(H解释),解释I： 谓词公式G在论域D上任何一组真值的指定称为一个解释。 H解释： 子句集S在的H域上的解释称为H解释。 问题： 对于所有的解释, 全是假才可判定。因为所有解释代表了所有的情况, 如可穷举, 问题便可解决 。,131,由子句集S建立H域、原子集A，希望定义于一般论域D上使S为真的任一解释I，可由依于S的H域上的某个解