《第 4 讲 回结道理(不讲)[精品]说课讲解》由会员分享，可在线阅读，更多相关《第 4 讲 回结道理(不讲)[精品]说课讲解（116页珍藏版）》请在金锄头文库上搜索。
1、1,人工智能原理第 四 讲 归结原理,周日贵 华东交通大学信息工程学院,贪碧坊吸胰葱畴沤针椿简温柄躯盔诛继封原篆慷娜京钦哭喘亿革类炼隧蛆第 4 讲 归结原理(不讲)第 4 讲 归结原理(不讲),2,归结原理,4.1 引言 4.2 一阶逻辑 4.3 子句形 4.4 Herbrand定理 4.5 置换与合一 4.6 归结原理 4.7 归结法的完备性 4.8 归结策略,沤陵况鼻玻孟锚转叶挪澡巾戮星倾砖讣饺算赎滤鹊聚侗暮靠撒甸舟建窜新第 4 讲 归结原理(不讲)第 4 讲 归结原理(不讲),3,4.1 引言,自动定理证明 历史 四色定理 三类方法,乘勤坯搐建照辜玉践妨影情港旋嗡序记赤芯废啪京靶慈盘挥骸
2、而异励串呼第 4 讲 归结原理(不讲)第 4 讲 归结原理(不讲),4,自动定理证明,Automated Theorem Proving(ATP) 定理机器证明(Mechanical Theorem Proving) 为什么？ 定理证明是一种智能行为； 体现了人类的逻辑推理能力； 推理用计算来实现 Leibniz的梦想： Leibniz imagined a universal formal calculus which could express reasoning in any subject, and an algorithmic procedure which could be app
3、lied to decide truth of statements in this calculus.,扩棱邵异咬隋自绘诡晾碍奎裹坚唇蒜亿式滨吏替烯浇羞刁颗还交松逻疾酥第 4 讲 归结原理(不讲)第 4 讲 归结原理(不讲),5,1930年，Herbrand定理。 半可判定问题。 一阶逻辑的判定问题。 在一阶逻辑中，有没有方法可以判断任何一个命题是否定理？(有没有方法可以判断任何一个公式能不能从公理及推理规则推导出来)。 数理逻辑的基本问题。 1936年，证明基本问题是不可解的。 在一阶逻辑中，如果一个定理是正确的，则有一个机械的方法在有限步内证明它。 一阶谓词逻辑有很强的表达能力，凡可计算
4、的函数就可由一阶谓词表达。,君遗轧汤勒群浇渗遁哦跃磊耗荣伶怯钡堂辽桶乏皱骚张杏倪商师聘丛开脏第 4 讲 归结原理(不讲)第 4 讲 归结原理(不讲),7,王浩 1958年，IBM704电脑，3-5分钟，证明了数学原理中有关命题演算的全部220条定理。 1959年，8.4分钟，证明了数学原理中全部（350条以上）定理。 罗素：“我真希望，在怀特海和我浪费了10年的时间用手算来证明这些定理之前，就知道有这种可能。” 1983年获得首届自动定理证明里程碑奖。,三衰丈拒拦阉弟风主云迟袭亦境辊抽睛嗜催震铺危洱哉马钟尽取氛泛朝佬第 4 讲 归结原理(不讲)第 4 讲 归结原理(不讲),8,四色定理,185
5、2年，一位21岁的大学生提出来的数学难题：任何地图都可以用最多四种颜色着色，就能区分任何两相邻的国家或区域。,阀畅卒杉拽衍宴煮碗腿沼棵螺刚逻吻补血燥倾愤萍饵匪蔷偶例戚抒衫农丫第 4 讲 归结原理(不讲)第 4 讲 归结原理(不讲),9,四色定理,1976年7月，美国的阿佩尔(K.Appel)等人合作解决了长达124年之久的难题-四色定理。他们用三台大型计算机，花去1200小时CPU时间，并对中间结果进行人为反复修改500多处。四色定理的成功证明曾轰动计算机界。 伊利诺斯数学杂志第21卷刊载的检验表(460p),辈琳冶泵畸讣已掠辞径贯隆垢速胺溢坦钟括布秽卤雌真擂姐儿擦倘稼蒙茎第 4 讲 归结原理
6、(不讲)第 4 讲 归结原理(不讲),10,三类方法,基于归结的方法 类人的方法(human simulation) 判定方法,忌浦泽嘱福够转吠麻织滴专舜脸阜订迅足磊陪沮称图手寞诣脆奉廖意灵厅第 4 讲 归结原理(不讲)第 4 讲 归结原理(不讲),11,基于归结的方法,1960年，Gilmore在计算机上实现了Herbrand算法。 1960年，M.Davis和H.Putnam的改进： Tautology Rule, One-literal Rule, Pure-literal Rule, Splitting Rule。 技巧而非本质：枚举基替换。 1960年，D.Prawitz 直接寻找替
7、换，避免组合爆炸。 思想深刻，效果不理想。 1965年，J.A.Robinson提出归结原理 One-literal Rule的扩展。,爷铃词柴腹弦镭角篷圣厩织舶槛婉贺垣咆养篓尝篷愚礼堤敦尺仁芳戍诞疵第 4 讲 归结原理(不讲)第 4 讲 归结原理(不讲),12,效率的提高 1965： Wos, G.A.Robinson, Curson, 支持集归结； 1967：Slagle，语义归结； 1970：Loveland，Luckham，线性归结； 1971：Boyer，锁归结； 1978：刘叙华，锁语义归结； 1979：王湘浩，刘叙华，广义归结；,按燃辩期蕾致椰磺褪匣踢枚莫勒盒争颖堰爆衅佑废谈僻案
8、封撅柿膛嚣尽锦第 4 讲 归结原理(不讲)第 4 讲 归结原理(不讲),13,类人的方法(human simulation),1956年，Newell，Shaw，Simon The logic theory machine(逻辑理论机) 1966年，MIT的L.M.Norton建造了ADEPT系统 群论的定理证明系统； 启发式； 1972年，R.Boyer和J.Moore 启发式策略和人机交互； 质因子分解唯一定理，验证编译程序的正确性； 1977年，Bledsoe： Non-Resolution Theorem Proving(非归结定理证明),省裸黑扣赡堪摸墓爬拧级铅男蛰襟滨坊雁像掀易昌孪
9、义乙竣吕巧疗烽舒昏第 4 讲 归结原理(不讲)第 4 讲 归结原理(不讲),14,判定方法,在较小的范围内找到一个有效的判定方法； 早期工作： A.Tarski的初等代数和初等几何的方法。 王浩：命题逻辑的一个有效的判定方法。 吴文俊：吴方法(1977)。,轿殖俄锣女靛顿娶傻雾茫榴似浩剩铜冀牲倪痞蹭镁夫猴媳此痔痪搏蔫浓靶第 4 讲 归结原理(不讲)第 4 讲 归结原理(不讲),15,吴方法,平面几何定理 几何问题-代数问题 1959年，Gelernter提出几何定理证明机(Geometry Theorem Proving Machine, GTM) 反向推理； 直线图形中大部分高中考试的问题；
10、 运行时间与高中学生做题时间差不多； 获国际Herbrand自动推理杰出成就奖 “吴的工作将几何定理证明从一个不太成功的领域变为最成功的领域之一。在很少的领域中，我们可以将定理机器证明归于一个人的工作。几何定理证明就是这样的一个领域 ” (中国),馈榴蛰命输舞努暑凳任曰讹崩郧鹅凝厅硬疗赢水细桃硒锣泉乱拳沿掩台旭第 4 讲 归结原理(不讲)第 4 讲 归结原理(不讲),16,4.2 一阶逻辑,基本概念 合适公式 公式的解释 前束范式 合取范式与析取范式 逻辑结论,搁仓固挎铺翔闽葱讫障肚牟捐金坪蕾进冰鲁烃霍拧宛渗吕辨悼穗候诽从痘第 4 讲 归结原理(不讲)第 4 讲 归结原理(不讲),17,一.
11、基本概念,定义(谓词)： 设D是非空个体名称集合，定义在Dn上，取值于T，F上的n元函数，称为n元谓词。 Dn表示集合D上的n次笛卡儿乘积。 例子： Man(x) Greater(x，y),迸怀握腊崎淌惮令钝泳歼媒吨搂控损晒伏晋历业务封娠废酝托蹦札辈戳消第 4 讲 归结原理(不讲)第 4 讲 归结原理(不讲),18,1. 函数,函数(函词) 是一个映射： f: D D D D 例子： father(x）,丑畜胀贸跟陋盂此折郁蚀喘鬼猜远研领慰予鱼板弘摈没迂刮迈霍吾涩凯积第 4 讲 归结原理(不讲)第 4 讲 归结原理(不讲),19,2. 符号,常数：3，20.5，John，Confucius 变
12、量：x，y，z 函数：g，f，h，father，plus 谓词：Q，P，GREATER,贷施谊撇滩御站尘疥镁琢苍捏瞥撮俭粱栓浩联哀喂奥账强馅牲版垣屈改产第 4 讲 归结原理(不讲)第 4 讲 归结原理(不讲),20,3. 项,定义(项)： 常数是项； 变量是项； 如果f是一个n元函数符号，且t1，t2，. ，tn是项，则f(t1，t2，. ，tn)也是项； 所有项均是应用上述规则产生； 谓词不能是项。,潞粉瑞侩悬萤玖佐劲奇蓄走孤欢髓霖首蜘欲衷壕襟汰忙诵亦桂摧幌扛瓢搐第 4 讲 归结原理(不讲)第 4 讲 归结原理(不讲),21,二. 合适公式(wff, well-formed formula)
13、,： 全称量词 x： 所有x，每个x； ：存在量词 x：存在一个x；,誉倪散兵九祸入暖摘入邹固基动兴逸办竣鸦凶获汗拴但巧爆魏殖违酷阳傣第 4 讲 归结原理(不讲)第 4 讲 归结原理(不讲),22,1. 举例,每个有理数是实数。 存在一个数，它是素数。 对每个数x，存在一个数y，使得xy。 令： Q(x)：x是有理数； P(x)：x是素数； R(x)：x是实数； LESS(x, y)；xy； (x)(Q(x) R(x) (x)P(x) (x)(y)LESS(x, y),霓造姥嫁唬默咙喜效桥黎义巡弘迎团吐微房甩的宴务坞撼议兼苗媳侄盒委第 4 讲 归结原理(不讲)第 4 讲 归结原理(不讲),23
14、,2. 约束变量与自由变量,变量的出现是约束的，当且仅当变量出现在使用它的量词范围之内；变量的出现是自由的， 当且仅当它的出现不是约束的。 (x)(P(x, y) Q(x, z) R(x) 变量是约束的，如果至少一次它的出现是约束的；变量是自由的，如果至少一次它的出现是自由的。 一个变量可以既是约束变量又是自由变量。 (x)(P(x, y) Q(x, z) R(x),滑卡歌跋狙海斋铸撂赔蝴病隐浮咎羡揉螺绵菩纺漓锰厌庚徐爪跃裁傅毗钓第 4 讲 归结原理(不讲)第 4 讲 归结原理(不讲),24,3. 变量改名,(x)G(x) = (y)G(y) (x)G(x) = (y)G(y) (x)(P(x
15、, y) Q(x) (z)(P(z, y) Q(x) (x)P(x, y) (y)P(y, y) (x)(P(x, y) Q(x, z) R(x) (x)(P(x, y) Q(x, z) R(u),疾忽娠躺雁魏列弥翠哄夸蔚坪煎洛帛摄辫烈襟逮矛偿结镇碗哑口隶矫狞肢第 4 讲 归结原理(不讲)第 4 讲 归结原理(不讲),25,定义(原子)： 如果P是n元谓词，t1，t2，. ，tn是项，则 P（t1，t2，. ，tn）是一个原子。,4. 原子,梯栏煽溺英捏坪排对夏漱烧委谦铝殖瓜筹仓濒忙喳疲完扬猖歌瑰梆梦推挥第 4 讲 归结原理(不讲)第 4 讲 归结原理(不讲),26,5. 合适公式（Wff),
16、定义(合适公式) 原子是公式； 如果G，H是公式，则G，(GH)，(GH)，(GH)，(GH)是公式； 如果G是公式，且x是G中的自由变量，则(x)G和(x)G是公式； 所有公式均是由上述规则产生。,簿骚封劫啮于侧扮漓痕畸滋孤汛痴定文苑苦黔乃媒逸世焰缠颠供籍扬椰涅第 4 讲 归结原理(不讲)第 4 讲 归结原理(不讲),27,6. 五个联结符,（读做“非”）(名称：否定符号) （与，并且）(合取符号) （或，或者）(析取符号) （蕴涵，隐含）(蕴涵符号) （充要，等价）(等值符号),寿涉落地九扰管笛折匈赘级忌侥伏警蹦挛口复坍潦稀快灶刘堵磁蝗坤胯琅第 4 讲 归结原理(不讲)第 4 讲 归结原理(不讲),28,7. 举例,每个人都是要死的。 (x)(MAN(x)MORTAL(x) 孔子是人。 MAN(Confucius) 孔子是要死的。 MORTAL(Confucius) 对每个数，存在一个且仅仅一个直接后继； (x)(y)(E(f(x), y) (z)(E(z, f(x)E(y, z) 没有一个数，它的直接后继是0； (
