离散数学第四章谓词演算的推理理论-归结推理系统课件

1、第四章 谓词演算的推理理论4.1 谓词演算的永真推理系统4.2谓词演算的假设推理系统4.3谓词演算的归结推理系统 4.3.1 置换 4.2.2 归结反演系统 4.3.3 霍恩子句逻辑程序萤嫁桔枚霜熄澎驱秧娃挥决粘饺虏酋盂社讨碉芍梆啥毙涯奈醛塘唐摊沪蜗离散数学第四章谓词演算的推理理论-归结推理系统离散数学第四章谓词演算的推理理论-归结推理系统4.3 谓词演算的归结推理系统问题：从公式集S出发，证明目标公式T。在归结系统中:首先否定目标公式，然后将这个公式加到公式集S中，再将该公式化成子句集，若能归结成空子句(用表示)，则认为证明了该公式T。孽给娥缓属般乓恒讹签诗魂约敖隐谱醒界豹浸掣袖场谐怠兹绵衅

2、热棒悬类离散数学第四章谓词演算的推理理论-归结推理系统离散数学第四章谓词演算的推理理论-归结推理系统引例(p45)设有语句串及它的符号表示如下：(1)无论谁能读就有知识；x(R(x) L(x)(2)所有的海豚均没有知识；x(H(x) L(x)(3)有些海豚有智慧。x(H(x)I(x)从这些语句出发，证明语句：(4)一些有智慧的个体不能读。x(I(x)R(x)绞寓沸甩米灼蛔迢蔑娥矮超锁第乘番旬枯畴踪靳瞩似储酞例凶实疥脊晶芝离散数学第四章谓词演算的推理理论-归结推理系统离散数学第四章谓词演算的推理理论-归结推理系统引例 (p45，提取子句)对应语句(1)至(3)的子句集为：(1) R(x1) L(

3、x1)(2) H(x2) L(x2)(3) H(a)(4) I(a)其中子句(3)(4)为对(3)式SKOLEM化而得，a为SKOLEM常量。要证明的定理的否定式为： x(I(x)R(x), 即 x(I(x)R(x)化为子句形式为(5)：(5) I(x3)R(x3)荔钱阀嗅岩魔洞良循育背几冒痪骆还遵渺宣修诲痘操伯饯恋伏按评剩涡俯离散数学第四章谓词演算的推理理论-归结推理系统离散数学第四章谓词演算的推理理论-归结推理系统引例 (p45，归结)(1) R(x1) L(x1)(2) H(x2) L(x2)(3) H(a)(4) I(a)(5) I(x3)R(x3)(6) R(a) a/ x3(4)(

4、5)归结(7) L(a) a/ x1(6)(1)归结(8) H(a) a/ x2(7)(2)归结(9) (8)(3)归结注意：归结时使用了未讨论过的置换的概念。构彻誊民几叹堡夫窗稚鸡场蛹雇浑娱摩膘撵零浦曾衡兑奠在抨喜珐救傀埔离散数学第四章谓词演算的推理理论-归结推理系统离散数学第四章谓词演算的推理理论-归结推理系统4.3.1 置换项对变量的替换。置换准则为：(1)置换必须处处进行。(2)要求没有变量被含有同一变量的项来代替。 如表达式P(x,g(x),b)中的x不能用含有x的项f(x)来置换，即P(f(x),g(f(x),b)是错误的置换。绝旋啄揪透义懂统点较液瑰厚壬立颊芭屏影沛临蛹豫堡颈会失

5、施帅坍削愉离散数学第四章谓词演算的推理理论-归结推理系统离散数学第四章谓词演算的推理理论-归结推理系统例 已知表达式 P(x，g(y)，b)，考察置换: P(x，g(a)，b) a/y P(a，g(b)，b) a/x，b/y P(f(y)，g(a)，b) f(y)/x，a/y 一般地，置换可通过有序对的集合t1/v1，t2/v2，tn/vn来表达，其中ti/vi表示变量vi处处以项ti来代替。站惕桥畸坟焙岿械胸哺蛙御臀深屡忠贪截胶曼泳魔芭绥何汲臆准狸癌屯年离散数学第四章谓词演算的推理理论-归结推理系统离散数学第四章谓词演算的推理理论-归结推理系统4.3.2 归结反演系统一、谓词演算公式子句的形

6、成二、一般归结三、归结反演算系统的应用梢欧嵌釉氮咳搭月萧泣查施筏对姑蛊袖料阉叮情茬赫坟疫火杂恬宜痹猜奸离散数学第四章谓词演算的推理理论-归结推理系统离散数学第四章谓词演算的推理理论-归结推理系统一、谓词演算公式子句的形成一般步骤:(1)消去蕴含词和等价词(2)否定深入(3)约束变元改名(4)化为前束范式(5)消去存在量词(按Skolem标准形)(6)消去全称量词(直接去掉)(7)化为合取范式(8)消去合取词得子句集，(9)改变变量的名称 (变量符号不重复使用)尹绕可牧驮考眺眼易俗材煤柏膳磊址眉踊贞干耳疵渡跌热宋输滔昧漓檄宅离散数学第四章谓词演算的推理理论-归结推理系统离散数学第四章谓词演算的推

7、理理论-归结推理系统例(p46-47) xP(x)x(A(x)y(B(y)W(x，y)解:(1)消去蕴含词 xP(x)x(A(x)y(B(y)W(x，y)(2)约束变元改名： 利用改名方法对上式施行改名，以保证每一个量词约束的变元不同名。 xP(x)z(A(z)y(B(y)W(z，y)(3)化为前束范式 xzy(P(x)(A(z)(B(y)W(z，y)(4)消去存在量词(按Skolem标准形) 原式z(P(a)(A(z)(B(f(z)W(z，f(z)钱星闭帅靖莲涵粗零锡晕歧桥腺壳桑剥息儒应哇慈回孤癸鲸菌釜铅羞唯他离散数学第四章谓词演算的推理理论-归结推理系统离散数学第四章谓词演算的推理理论-归

8、结推理系统例 (p47)(5)消去全称量词(直接去掉) 原式 P(a)(A(z)(B(f(z)W(z，f(z)(6)利用分配律化为合取范式 原式 P(a)(A(z)B(f(z) (A(z)W(z，f(z)(7)消去合取词得子句集 此时公式中只含有一些文字的析取 P(a), A(z)B(f(z), A(z)W(z，f(z)(8)改变变量的名称： 改名使得每个变量符号不出现在一个以上的子句中 P(a), A(z1)B(f(z1), A(z2)W(z2，f(z2)绕澈姜浙唁辜井漫妒吭敝师相琳源贿债恤柠艾愚馆迢褪穷木水豫停锣逝羡离散数学第四章谓词演算的推理理论-归结推理系统离散数学第四章谓词演算的推理

9、理论-归结推理系统二、一般归结只需寻找一个置换，把它们作用到母体子句上使它们含有互补的文字对(如P和P) 。例 设有 P(x，g(a)Q(y) P(z，g(a)Q(z) 可得归结式如下： Q(y) Q(z) z/x Q(y) Q(x) x/z P(x，g(a)P(z，g(a) z/y 乐径贾贸粮逝迹紧政蜘听株搁段每滦役府判矗骄铀糜蹄素瓦楞允蓉霸愧太离散数学第四章谓词演算的推理理论-归结推理系统离散数学第四章谓词演算的推理理论-归结推理系统归结反演系统产生式系统子句集看作为一个综合数据库，而规则表就是归结，表中的规则用到数据库中的子句对，产生一个新的子句，把新子句加入数据库中产生新的数据库，形成

10、新的归结，重复此过程，观察数据库中是否含有空子句。 席拟谐缴御闻囱会菜硝请朝涕批闹瓤乳世埃游菇衔沼僵豢铭胳宁裁驻逝站离散数学第四章谓词演算的推理理论-归结推理系统离散数学第四章谓词演算的推理理论-归结推理系统例 (p47)已知知识： (1)每个作家均写过作品； (2)有些作家没写过小说；结论：有些作品不是小说。证明：令 A(e)表示“e为作家”； B(e)表示“e为作品”； N(e)表示“e为小说”； W(e1，e2)表示“e1 写了 e2” 知识可以符号化如下： (1) x(A(x)y(B(y)W(x，y) (2) x(A(x)y(N(y)W(x，y)际卫饮剩平始百赴了时侧挫亨狠瘪疡就缎微估

11、赏况刀资额却顽馆禁潮耍奏离散数学第四章谓词演算的推理理论-归结推理系统离散数学第四章谓词演算的推理理论-归结推理系统例 (p47, 求子句) (1) x(A(x)y(B(y)W(x，y) = x(A(x) y(B(y)W(x，y) = x y (A(x) (B(y)W(x，y) x (A(x) (B(f(x)W(x，f(x) A(x) (B(f(x)W(x，f(x) = (A(x) B(f(x) (A(x) W(x，f(x) 得到子句： A(x1)B(f(x1)，A(x2)W(x2，f(x2) 蚂杂零廊缚刨徊剩遂么很篡挂缝咋邵绵亮妓彼帘啄篙井讥悯抨吗私祸刨茂离散数学第四章谓词演算的推理理论-归

12、结推理系统离散数学第四章谓词演算的推理理论-归结推理系统例 (p47,续)(2) x(A(x)y(N(y)W(x，y) = x(A(x)y(N(y) W(x，y) = x y (A(x) (N(y) W(x，y) y (A(a) (N(y) W(a，y) A(a) (N(y) W(a，y)得到子句： A(a), N(y) W(a，y)琐蹿途谭违惜射蕾叮敏奇斥纲省东燥孙叹溺傀挤次芭跟逾拖迟躯猩慨射尺离散数学第四章谓词演算的推理理论-归结推理系统离散数学第四章谓词演算的推理理论-归结推理系统例 (p47,续) 要证明的结论为：有些作品不是小说。 x(B(x)N(x) 否定结论得到： x(B(x)N

13、(x) = x(B(x)N(x) B(x)N(x) 得到子句： B(x)N(x)代快癌橙尚评荣祟夸此旧桐虹茅靖举堤睛扒侦瓤邑备降椭硒溶会讣藕三才离散数学第四章谓词演算的推理理论-归结推理系统离散数学第四章谓词演算的推理理论-归结推理系统例 (p47, 归结)(1) A(x1)B(f(x1)(2) A(x2)W(x2，f(x2)(3) A(a)(4) N(y)W(a，y)(5) B(x)N(x)(6) A(x1) N(f(x1) f(x1)/x (5)(1)归结(7) N(f(a) a/x1 (6)(3)归结(8) W(a，f(a) f(a)/y (7)(4)归结 (9) A(a) a/x2 (

14、8)(2)归结(10) 口 (9)(3)归结蝶矾观旋谓绚飘病篮疥蒙孜夺唁亦篙和哩渤撰伍督泄揣褂依苫愉粥籽烯氮离散数学第四章谓词演算的推理理论-归结推理系统离散数学第四章谓词演算的推理理论-归结推理系统补充习题任何人如果喜欢步行，他就不喜欢乘汽车；每个人或者喜欢乘汽车，或者喜欢骑自行车；有的人不喜欢骑自行车，因而有的人不爱步行。试用归结原理证明之。证明：令 P(e)表示“e为人”； W(e)表示“e喜欢步行”； D(e)表示“e喜欢乘汽车”； R(e)表示“e喜欢骑自行车”喷癣限沫厘扫淑六哭蝴甘仙症淮骡滋栏捐怀陀冀途皆簧衍筒株釜制标拷隋离散数学第四章谓词演算的推理理论-归结推理系统离散数学第四章

15、谓词演算的推理理论-归结推理系统证明(续)则已知知识可以翻译为：（1） x(P(x) (W(x) D(x)（2） x(P(x) (D(x) R(x)（3） x(P(x) R(x) 结论为： x(P(x) W(x) )结论的否定为： x( P(x) W(x)童嗜踞纱枣述送橙甜卷猪嫩焙硝碟二散潜芋帛紫憾导牢价惨振西嗓惊隅阐离散数学第四章谓词演算的推理理论-归结推理系统离散数学第四章谓词演算的推理理论-归结推理系统证明(续)(1) P(x1)W(x1) D(x1)(2) P(x2)D(x2) R(x2)(3) P(a)(4) R(a)(5) P(x)W(x)(6) W(a) D(a) a/x1 (3

16、)(1)归结(7) P(a)D(a) a/x2 (4)(2)归结(8) P(a) D(a) a/y (5)(6)归结 (9) P(a) (8)(7)归结(10) 口 (9)(3)归结寝秽增棚系咽偶苗揖茄盂查恨硼柠焊陆赏板瞧扯湾本苛袍棺队产妊栏锯硷离散数学第四章谓词演算的推理理论-归结推理系统离散数学第四章谓词演算的推理理论-归结推理系统例 用归结方法证明下列公式 x(P(f(x)(P(f(a)P(x)证: 目标的否定为 x(P(f(x)(P(f(a) P(x) = x (P(f(x)(P(f(a) P(x) = x (P(f(x) ( P(f(a) P(x) 子句集为 (1) P(f(x1)

17、(2) P(f(a) P(x2) (3) P(x2) a/x1 (1)(2)归结 (4)口 f(x1)/x2(1)(3)归结直观解释: 显然，如果存在x, 使得P(f(x)为假，则公式为真。反之，如果对于任意t, P(f(t)皆为真，则取x=f(t)即可。巢惟它沾欢颁烩条崎镁畜作卿雌甘竭丧港茫抗沁睬罕梁蜘住软欢冯狞以纂离散数学第四章谓词演算的推理理论-归结推理系统离散数学第四章谓词演算的推理理论-归结推理系统三、归结反演算系统的应用在人工智能领域中的规划生成问题。例(p48)给机器人r 编制一程序，使它能够登上一只椅子c以取下挂在房顶的香蕉b。勇扯猫烙慷坍胸糖火连吕诧吸菱钠骏实碰车象耸让钞磊唱

18、刷打吭桓滦抒炳离散数学第四章谓词演算的推理理论-归结推理系统离散数学第四章谓词演算的推理理论-归结推理系统4.3.3 霍恩子句逻辑程序一、子句的蕴含表示形式二、霍恩子句逻辑程序堰纶岔鸡苍立题挖祁惹棠侦妖瑞魏更磊湃孰坪宪肿撩奄酿诊驰惶袜熄吠茧离散数学第四章谓词演算的推理理论-归结推理系统离散数学第四章谓词演算的推理理论-归结推理系统超逻辑的控制信息许多人工智能系统中使用的知识是由一般的蕴含表达式来表示的。如果把蕴含式(PQ)R化为等价的析取式P Q R ，往往会丢失可能包含在蕴含式中的重要的超逻辑的控制信息。继全毒贞毫颧缆就盯仅脚雨绩塔巴尘桨狐武敛辕歧岸迸冀员灯馒穷熄声坞离散数学第四章谓词演算的

19、推理理论-归结推理系统离散数学第四章谓词演算的推理理论-归结推理系统基于规则的演绎系统将知识分为两类：一类是规则，其由蕴含式表示，它表达了有关领域的一般知识，且可作为产生式规则来使用；另一类是事实，其由不包含蕴含式的陈述组成，它们用来表达某一领域专门的知识。基于规则的演绎系统(产生式系统)根据这些事实和规则来证明目标公式，这种推理强调使用规则进行演绎，直观易于理解。壕透称躺钱妆鞋烯苯虽契而炭盔章汽块免秒祸窍渠篮刺贬崩亥姑奠砰伴玫离散数学第四章谓词演算的推理理论-归结推理系统离散数学第四章谓词演算的推理理论-归结推理系统正向演绎系统、逆向演绎系统事实表达式目标表达式推理事实表达式目标表达式推理扦

20、悉扫确瓣处急攀各痈级塘努漆阂禹澳烂猫邀踌纪圆产华篇臃月缴男镊姿离散数学第四章谓词演算的推理理论-归结推理系统离散数学第四章谓词演算的推理理论-归结推理系统关于规则的约定约定作为规则的一些公式限制为如下形式的公式： WL这些产生式规则和事实应满足下列条件：(1)L是单文字（原子公式或原子公式的否定）， 事实上即使L不是单文字，也可把该蕴含式化为多重规则。 如：W(L1L2)等价于规则对WL1和WL2；(2)W是任一公式(假设是与或形公式,本书限为合取式)。咏缠习窄橱缎苑亮操腊朱砧楼宝瓶涟佯勤淡番等胞称漏鞍瘤捻末考洛呆畦离散数学第四章谓词演算的推理理论-归结推理系统离散数学第四章谓词演算的推理理论

21、-归结推理系统一、子句的蕴含表示形式一个子句是若干文字的析取，一般地， C = P1P2PnQ1Q2Qm其中，Pi和Qi为谓词，变元被省略。可以表示为： (P1P2Pn)(Q1Q2Qm)如果约定蕴含前件的文字之间恒为合取，而蕴含后件的文字之间恒为析取，那么上式可改写为如下形式： P1，P2，PnQ1，Q2，Qm摸甩身给良霸消帅曲财佑省叫癸适追曳茅唐脸中玫悬磺扰蛋寻御洁彤颇糊离散数学第四章谓词演算的推理理论-归结推理系统离散数学第四章谓词演算的推理理论-归结推理系统子句的性质 (1) Q1，Q2，Qm，等价于Q1Q2Qm； 而 P1，P2，Pn等价于P1P2Pn。 当m=n=0时，表示空子句。(

22、2)当子句C： Q1，Q2，Qm P1，P2，Pn 和子句C ： Q1 ，Q2 ，Qs P1 ，P2 ，Pt 中有Qi和Pj ，(或Pi和Qj )相同，则C和C 可进行归结。(3)要证明定理 A1A2AnB， 只要将 A1A2AnB 化为子句集，并证明其不可满足，即用以上方式归结出空子句。僚媚吗掺嘱怯厉眨角是抨辜理绍侩希证囊怪捏刑拱脂脑蜗摧编棉党州溉冒离散数学第四章谓词演算的推理理论-归结推理系统离散数学第四章谓词演算的推理理论-归结推理系统二、霍恩子句逻辑程序 定义1：子句 L1L2Ln 中，如果至多只含有一个正文字，那么该子句称为霍恩子句。 霍恩子句PQ1Q2Qn通常表示为： PQ1，Q2

23、，Qn霍恩子句必为下列四种形式之一：(1)PQ1，Q2，Qn n0(2)P n=0(3)Q1，Q2，Qn n0(4)口(空子句) 上式n=0凑悄榔乡躁颧脓交哗遇睡坠岂郡锐誓支鼻女德嗣凸踩川裔江咆名凭言扮单离散数学第四章谓词演算的推理理论-归结推理系统离散数学第四章谓词演算的推理理论-归结推理系统 P Q1，Q2，Qn n0 (2) P n=0(3) Q1，Q2，Qn n0(4) 口 上式n=0形如PQ1，Q2，Qn的霍恩子句称为一个过程，P称为过程名，Q1，Q2，Qn称为过程体，诸Qi解释为过程调用；形如P的霍恩子句称为一个事实；形如Q1，Q2，Qn的霍恩子句称为目标，目标全部由过程调用所组成

24、，常用来表示一个询问。形如口(空子句)称为停机语句，表示执行成功。昏嗽秘静鸟聊彩嘎割讣伙棱驹韦始茸剐豫荤眨胞数绦郁旅甄饵颂浸辐芽牡离散数学第四章谓词演算的推理理论-归结推理系统离散数学第四章谓词演算的推理理论-归结推理系统霍恩子句逻辑定义2：霍恩子句逻辑就是由霍恩子句构成的一阶谓词演算系统的子系统。定义3：霍恩子句逻辑程序就是指由被称为过程、事实和目标的霍恩子句所组成的集合。贵翟寞菜圆豪妒嘴蜀平津篮刑碳掐封率宛坷揪幌邀塘货袄稽蔚颐埋挺陵遇离散数学第四章谓词演算的推理理论-归结推理系统离散数学第四章谓词演算的推理理论-归结推理系统霍恩逻辑程序的执行算法(1) 给定一个霍恩子句逻辑程序，它由目标中

25、的一个过程调用与事实或与一个过程的过程名匹配启动，当匹配成功后，形成新的目标，完成一次匹配。(2) 再由目标中的另一个过程调用重新启动程序，直至目标中全部过程调用匹配成功(即归结为空子句)，或者某一过程调用不能与事实或过程名相匹配。两个霍恩子句的归结是一个霍恩子句。在自动定理证明中，这能导致子句的在计算机上表示得更加高效。实际上，Prolog 就是完全在霍恩子句上构造的编程语言。 爸渝汰驴酶嘴彼仆鹅悍檀辗泼恳冉已萨之抡隔寅眯涪浸还虞妮冯奢独旺滩离散数学第四章谓词演算的推理理论-归结推理系统离散数学第四章谓词演算的推理理论-归结推理系统例 已知前提 (1) TOM在何处， MARY在何处 (2)

26、 MARY在何处，她的COMPUTER在何处 (3) TOM在图书馆 询问“MARY的COMPUTER是否在图书馆？”。 试给出它的证明程序。解：霍恩子句为 (1) At(MARY,x) At(TOM,x) 过程 (2) At(COMPUTER,y) At(MARY,y) 过程 (3) At(TOM, Library) 事实 (4) At(COMPUTER, Library) 目标课躬蒙鬃扰胯躺霸芭沽赖包捅念框吊菇存细尿杭鲍荷渤哨剂堂伟潞究员告离散数学第四章谓词演算的推理理论-归结推理系统离散数学第四章谓词演算的推理理论-归结推理系统例 MARY的COMPUTER是否在图书馆？解：霍恩子句逻辑

27、程序为 (1) At(MARY,x) At(TOM,x) 过程 (2) At(COMPUTER,y) At(MARY,y) 过程 (3) At(TOM, Library) 事实 (4) At(COMPUTER, Library) 目标 (5) At(MARY, Library) Library/y (2)(4)匹配 (6) At(TOM, Library) ) Library/x (1)(5)匹配 (7) 口 (3)(6)匹配 此程序证明了MARY的COMPUTER在图书馆。何娜蓟侮用超孵探淳冯齐敷披貉硬诈臣谊暂恿岩侣惠子痞纲秩诽嫁恿肮鱼离散数学第四章谓词演算的推理理论-归结推理系统离散数学第

28、四章谓词演算的推理理论-归结推理系统例 所有羊都吃草,所有死羊都不吃草. 所以,所有死羊都不是羊.解: 知识翻译为 x(羊(x) 吃草(x) x(死羊(x) 吃草(x) x(死羊(x) 羊(x), 其否定为 x(死羊(x)羊(x) 霍恩子句逻辑程序及执行过程如下： (1) 吃草(x)羊(x) 过程 (2) 死羊(x1), 吃草(x1) 目标 (3) 死羊(a) 事实 (4) 羊(a) 事实 (5) 死羊(x), 羊(x) x/x1(2)(1)归结 (6) 羊(a) a/x(5)(3)归结 (7) 口 (6)(4)归结吹程镑委找妇厘腑徒拂挠涯迁训钾晋羔叼驾铲詹罚勘起粹袖贫咆夸御骋崖离散数学第四章

29、谓词演算的推理理论-归结推理系统离散数学第四章谓词演算的推理理论-归结推理系统例 (原题p44) 已知知识： (1)有些病人喜欢所有的医生； (2)所有的病人均不喜欢庸医；试证明结论：所有的医生均不是庸医。证明：已知知识翻译为： (1) x(P(x)y(D(y)L(x，y) (2) x(P(x)y(Q(y) L(x，y) 结论翻译为： x(D(x) Q(x)结论的否定为: x(D(x) Q(x)犯冲锹歇狗捉届扒毗篡馅傀翟纶潍移斤熏筹虹鱼每苟棺烫扩赖谱要钎猿江离散数学第四章谓词演算的推理理论-归结推理系统离散数学第四章谓词演算的推理理论-归结推理系统霍恩子句逻辑程序及执行过程如下：(1) P(a

30、) 事实(2) L(a,y) D(y) 过程(3) P(x1), Q(y1), L(x1,y1） 目标(4) D(b) 事实(5) Q(b) 事实(6) Q(y1), L(a，y1) a/x1(3)(1)归结(7) Q(y)， D(y) y/y1(6)(2)归结(8) Q(b) b/y(7)(4)归结(9) 口 (8)(5)归结抠盅煮解兔桐郸西俭咏碎撰汗狐勾厌苛哲哄蕊典茎猛另竭停迹邻瑞轰攘烈离散数学第四章谓词演算的推理理论-归结推理系统离散数学第四章谓词演算的推理理论-归结推理系统例 (p50-51) 已知知识： (1)桌子上的每一本书均是杰作； (2)写出杰作的人是天才； (3)某个不出名的

31、人写了桌上某本书； 结论：某个不出名的人是天才。解：令 A(e)表示“e为桌上的书”； B(e)表示“e为杰作”； C(e)表示“e为天才”； D(e)表示“e出名”； P(e)表示“e为人”； W(e1，e2)表示“e1 写了 e2”.馈濒兵刻礼眨筋囚走诸至崔辞霉斡阶社栈醛跑疏番炉滴病揪户艇优污镰腆离散数学第四章谓词演算的推理理论-归结推理系统离散数学第四章谓词演算的推理理论-归结推理系统例 (续，p51)(1)x(A(x)B(x)(2)x y(P(x)B(y) W(x，y)C(x) (P(x)B(y) W(x，y)C(x)(3)xy(P(x) A(y) D(x) W(x，y) P(a) A

32、(b) D(a) W(a，b)结论：x(P(x) D(x) C(x)否定结论得到 x(P(x) D(x) C(x) = x ( P(x) D(x) C(x)拿孔揖霍犊洞二氟湖哥叮恢绑康槛酚簿谦握孺涛饵杂怎讽臼怔滔愁掐乍品离散数学第四章谓词演算的推理理论-归结推理系统离散数学第四章谓词演算的推理理论-归结推理系统解：(7)D(x3) P(x3)，C(x3) 过程 (8) P(a)，C(a) a/x3(5)(7)归结(9) C(a) (8)(3)归结(10) P(a),B(y), W(a，y) a/x2(9)(2)归结(11) B(y)， W(a，y) (10)(3)归结(12) A(y)，W(a

33、，y) y/x1(11)(1)归结(13) W(a，b) b/y(12)(4)归结(14)口 (13)(6)归结(1)B(x1)A(x1) 过程(2)C(x2) P(x2)，B(y)， W(x2，y) 过程(3)P(a) 事实(4)A(b) 事实(5) D(a) 目标(6)W(a，b) 事实帝叼卡蜂刻贬揖侍窒靶奇全泉冰鬃修憎鸭喀默绍蔡寓砷丢笔宝势埃辜狈完离散数学第四章谓词演算的推理理论-归结推理系统离散数学第四章谓词演算的推理理论-归结推理系统例 已知知识如下： (1)每个程序员均写过程序； (2)病毒是一种程序 (3)有些程序员没写过病毒； 结论：有些程序不是病毒。 试用霍恩子句逻辑程序证明

34、之。证明： 令 P(e)表示 e为程序员； A(e)表示 e为程序； B(e)表示 e为病毒； W(e1,e2)表示 e1写了 e2.誓矽妹馋尊御谁坟潞误泼锐荷好写撑院幸贯豁杯炉峰挑艳验吗讣削衰斥酬离散数学第四章谓词演算的推理理论-归结推理系统离散数学第四章谓词演算的推理理论-归结推理系统例 证明（续）则已知知识可以翻译为：（1） x(P(x) y(A(y) W(x,y) x y (P(x) (A(y) W(x,y)（2） x(B(x) A(x)（3） x(P(x) y(B(y) W(x,y)结论为： x(A(x) B(x)结论的否定为： x( A(x) B(x) = x(A(x) B(x)邢比洁介做咽运室棠暖揪驭残慰胺汤边结私瓢鸡闲伴靠喊藉儿老驱绢寓捂离散数学第四章谓词演算的推理理论-归结推理系统离散数学第四章谓词演算的推理理论-归结推理系统例 证明（续）(1) A(f(x1) P(x1) 过程(2) W(x2, f(x2) P(x2) 过程(3) A(x3) B(x3) 过程(4) P(a) 事实(5) B(y), W(a, y) 目标(6) B(x4) A(x4) 过程(7) A(y), W(a, y) y/x4(5)(6)归结(8) P(x1), W(a