离散数学 第三章 消解原理

上传人:M****1 文档编号:545745302 上传时间:2023-04-04 格式:DOC 页数:9 大小:107KB
返回 下载 相关 举报
离散数学 第三章 消解原理_第1页
第1页 / 共9页
离散数学 第三章 消解原理_第2页
第2页 / 共9页
离散数学 第三章 消解原理_第3页
第3页 / 共9页
离散数学 第三章 消解原理_第4页
第4页 / 共9页
离散数学 第三章 消解原理_第5页
第5页 / 共9页
点击查看更多>>
资源描述

《离散数学 第三章 消解原理》由会员分享,可在线阅读,更多相关《离散数学 第三章 消解原理(9页珍藏版)》请在金锄头文库上搜索。

1、*第三章 消 解 原 理3.1 斯柯伦标准形 内容提要 我们约定,本章只讨论不含自由变元的谓词公式(也称语句,sentences),所说前束范式均指前束合取范式。 全称量词的消去是简单的。因为约定只讨论语句,所以可将全称量词全部省去,把由此出现于公式中的“自由变元”均约定为全称量化的变元。例如A(x)实指xA(x)。 存在量词的消去要复杂得多。考虑$xA(x)。 (1)当A(x)中除x外没有其它自由变元,那么,我们可以像在自然推理系统中所做那样,可引入A(e/x),其中e为一新的个体常元,称e为斯柯伦(Skolem)常元,用A(e/x)代替$xA(x),但这次我们不把A(e/x)看作假设,详见

2、下文。 (2)当A中除x外还有其它自由变元y1,yn,那么 $xA(x, y1,yn) 来自于y1yn$xA(x, y1,yn),其中“存在的x”本依赖于y1,yn的取值。因此简单地用A(e/x, y1,yn)代替 $xA(x, y1,yn) 是不适当的,应当反映出x对y1,yn的依赖关系。为此引入函数符号f,以A(f(y1,yn)/x, y1,yn) 代替 $xA(x, y1,yn),它表示:对任意给定的y1,yn, 均可依对应关系f确定相应的x,使x, y1,yn满足A。这里f是一个未知的确定的函数,因而应当用一个推理中尚未使用过的新函数符号,称为斯柯伦函数。 定理3.1(斯柯伦定理)对任

3、意只含自由变元x, y1,yn的公式A(x, y1,yn),$xA(x, y1,yn)可满足,当且仅当A(f(y1,yn), y1,yn)可满足。这里f为一新函数符号;当n = 0时,f为新常元。 定义3.1 设公式A的前束范式为B。C是利用斯柯伦常元和斯柯伦函数消去B中量词(称斯柯伦化)后所得的合取范式,那么称C为A的斯柯伦标准形(Skolem normal form)。 以下我们约定:斯柯伦标准形中,各子句之间没有相同的变元。 定义3.2 子句集S称为是可满足的,如果存在一个个体域和一种解释,使S中的每一个子句均为真,或者使得S的每一个子句中至少有一个文字为真。否则, 称子句集S是不可满足

4、的。 习题解答练习3.1 1、求下列各式的斯柯伦标准形和子句集。 (1)(xP(x)$yzQ(y, z) (2)x(E(x, 0)$y(E(y, g(x)z(E(z, g(x)E(y, z) (3)(xP(x)$y P(y)(4) (1)(2)(3)解(1)(xP(x)$yzQ(y, z)xP(x)$yzQ(y, z) $xP(x)$yzQ(y, z)斯柯伦标准形:P(e1)Q(e2, z)子句集:P(e1),Q(e2, z)(2)x(E(x, 0)$y(E(y, g(x)z(E(z, g(x)E(y, z) x$yz (E(x, 0)(E(y, g(x)(E(z, g(x)E(y, z) x

5、$yz (E(x, 0)E(y, g(x)(E(x, 0)E(z, g(x)E(y, z) 斯柯伦标准形:(E(x, 0)E(f(x), g(x)(E(x, 0)E(z, g(x)E(f(x), z)子句集: E(x, 0)E(f(x), g(x), E(x, 0)E(z, g(x)E(f(x), z)(3)(xP(x)$y P(y)xP(x)$y P(y)xP(x)yP(y)xy (P(x)P(y)斯柯伦标准形:P(x)P(y)子句集:P(x),P(y) (4)(1)(2)(3)斯柯伦标准形:P(e1)Q(e2, z)(E(x, 0)E(f(x), g(x)(E(u, 0)E(y, g(u)

6、E(f(u), y)P(w)P(v)子句集:P(e1),Q(e2, z), E(x, 0)E(f(x), g(x), E(u, 0)E(y, g(u)E(f(u), y), P(w),P(v)2、设公式A1,A2的子句集分别为S1,S2,如果S1与S2等值(表示对应的斯柯伦标准形有相等的真值),问是否一定有A1与A2等值,为什么?解 不一定有A1与A2等值。例如,个体域为自然数集合,A1为$y P(y),A2为$y Q(y),P(y)表示:y是偶数,Q(y)表示:y是负数。$y P(y)与$y Q(y)不等值,但P(e1)与Q(e2)在解释I把e1,e2确定为奇数时,却是等值的。3、假如要利用

7、子句集不可满足性来证明(PQ)(QR)(PR)永真。试作出待证公式否定的子句集。解 待证公式否定的子句集为: PQ, QR,P, Q4、要利用子句集不可满足性来证明例2.25的推理是正确的。试作出这一推理的否定(前提1前提2结论)的子句集。解5. 试简述A(e/x) 或A(f(y1,yn)/x, y1,yn) 可以在应用消解原理的推理中代替 $xA(x) 或 y1yn$xA(x, y1,yn) 的原因,以及选择e,f应注意的事项。解 A(e/x) 或A(f(y1,yn)/x, y1,yn) 可以在应用消解原理的推理中代替 $xA(x) 或 y1yn$xA(x, y1,yn) 的原因是:(1)

8、(1) 用消解原理证明定理A或证明 GA,是通过确认A和B1BnA(B1,Bn为G中公式)的不可满足性来实现的。(2) (2) A(e/x) ,A(f(y1,yn)/x, y1,yn)与$xA(x) ,y1yn$xA(x, y1,yn)的不可满足性是相同的。选择e,f应注意选择新常元和新函数符号,即在推理过程中尚未使用过的常元和函数符号。3.2 命题演算消解原理内容提要 关于命题演算的消解原理。设C1,C2为两个子句,L1,L2是分别属于C1,C2的互补文字对,用C-L表示从子句C中删除文字L后所得的子句,那么消解原理可表示为 其中C1,C2称为消解母式,L1,L2称为消解基,而(C1-L1)

9、(C2-L2)称为消解结果。 特别地,当C1,C2都是单文字子句,且互补时,C1,C2的消解结果不含有任何文字,这时我们称其消解结果是“空子句”(nil),常用符号 表示之, 空子句是永远无法被满足的。 关于消解原理我们有: 定理3.2 设C是C1,C2的消解结果,那么C是C1和C2的逻辑结果。 本定理的证明可仿以上对式(3.1)的证明,请读者自行完成。据本定理知,消解原理作为推理规则是适当的。 作为特别情况,p与p的消解结果是,实质上是pp的另一种表示形式,它们都是不可满足的,因而也满足定理3.2的结论。定义3.3 设S为一子句集,称C是S的消解结果,如果存在一个子句序列C1,C2 ,,Cn

10、(= C),使Ci(i = 1,2, ,n) 或者是S中子句,或者是Ck,Cj (k,j i) 的消解结果。该序列称为是由S导出的C的消解序列。当是S的消解结果时,称该序列为S的一个否证(refutations)。定理3.3 如果子句集S有一个否证,那么S是不可满足的。 习题解答练习3.21、 1、 完成定理3.2证明。证 设C1,C2为两个子句,L1,L2是分别属于C1,C2的互补文字对,用C-L表示从子句C中删除文字L后所得的子句,那么消解原理可表示为 设C1,C2分别为L1C1,L2C2 ; L1,L2为消解基, 即C1=C1- L1 ,C2= C2- L2。由于L2 = L1,那么(L

11、1C1)(L2C2)(L1C1)(L1C2) (L1C2)(C1L1)(C1C2) C1C2于是我们有 (L1C1)(L2C2)(C1- L1)(C2- L2)即C1C2(C1- L1)(C2- L2)。这就是说,C1与C2的消解结果是C1和C2的逻辑结果。 2、证明下列子句集是不可满足的。(1)S = pq, qr, pq, r解(1)pq (2)qr(3)pq(4)r(5)q 由(2)(4)消解得(6)p 由(1)(5)消解得(7)p 由(3)(5)消解得(8)(2)S = pq, qr, rw, rp, wq, qr解(1)pq (2)qr(3)rw(4)rp(5)wq (6)qr (7

12、)rq 由(1)(4)消解得(8)q 由(2)(7)消解得(9)w 由(5)(8)消解得(10)r 由(6)(8)消解得(11)r 由(3)(9)消解得(12) 由(10)(11)消解得 3、用消解原理证明下列逻辑蕴涵式。(1)(pq)r (pr)(qr)解 S = pr,qr, pq , pr, qr, r(1)pr (2)qr(3)pq(4)pr(5)qr (6)r (7)p 由(1)(6)消解得(8)q 由(2)(6)消解得(9)q 由(3)(7)消解得(10) 由(8)(9)消解得(2)(pr)(qr) (pq)r解 S = pr,qr, pq , r(1)pr (2)qr(3)pq(4)r (5)p 由(1)(4)消解得(6)q 由(2)(4)消解得(7)q

展开阅读全文
相关资源
相关搜索

当前位置:首页 > 幼儿/小学教育 > 小学课件

电脑版 |金锄头文库版权所有
经营许可证:蜀ICP备13022795号 | 川公网安备 51140202000112号