回结道理(不讲)[精品

回结道理(不讲)[精品

ID:27613264

大小:309.50 KB

页数:116页

时间:2018-12-01

回结道理(不讲)[精品_第1页
回结道理(不讲)[精品_第2页
回结道理(不讲)[精品_第3页
回结道理(不讲)[精品_第4页
回结道理(不讲)[精品_第5页
资源描述:

《回结道理(不讲)[精品》由会员上传分享,免费在线阅读,更多相关内容在教育资源-天天文库

1、人工智能原理第四讲归结原理周日贵华东交通大学信息工程学院贪碧坊吸胰葱畴沤针椿简温柄躯盔诛继封原篆慷娜京钦哭喘亿革类炼隧蛆第4讲归结原理(不讲)第4讲归结原理(不讲)1归结原理4.1引言4.2一阶逻辑4.3子句形4.4Herbrand定理4.5置换与合一4.6归结原理4.7归结法的完备性4.8归结策略沤陵况鼻玻孟锚转叶挪澡巾戮星倾砖讣饺算赎滤鹊聚侗暮靠撒甸舟建窜新第4讲归结原理(不讲)第4讲归结原理(不讲)24.1引言自动定理证明历史四色定理三类方法乘勤坯搐建照辜玉践妨影情港旋嗡序记赤芯废啪京靶慈盘挥骸而异励串呼第4讲归结原理(不讲)第4讲归结原理(不讲)3自动

2、定理证明AutomatedTheoremProving(ATP)定理机器证明(MechanicalTheoremProving)为什么?定理证明是一种智能行为;体现了人类的逻辑推理能力;推理用计算来实现Leibniz的梦想:Leibnizimaginedauniversalformalcalculuswhichcouldexpressreasoninginanysubject,andanalgorithmicprocedurewhichcouldbeappliedtodecidetruthofstatementsinthiscalculus.扩棱邵异咬隋自绘诡

3、晾碍奎裹坚唇蒜亿式滨吏替烯浇羞刁颗还交松逻疾酥第4讲归结原理(不讲)第4讲归结原理(不讲)41930年,Herbrand定理。半可判定问题。一阶逻辑的判定问题。在一阶逻辑中,有没有方法可以判断任何一个命题是否定理?(有没有方法可以判断任何一个公式能不能从公理及推理规则推导出来)。数理逻辑的基本问题。1936年,证明基本问题是不可解的。在一阶逻辑中,如果一个定理是正确的,则有一个机械的方法在有限步内证明它。一阶谓词逻辑有很强的表达能力,凡可计算的函数就可由一阶谓词表达。君遗轧汤勒群浇渗遁哦跃磊耗荣伶怯钡堂辽桶乏皱骚张杏倪商师聘丛开脏第4讲归结原理(不讲)第4讲归

4、结原理(不讲)5历史Newell,Shaw,Simon1956年,Thelogictheorymachine(逻辑理论机).数学定理证明程序(LogicTheorist)mimichumanreasoning《数学原理》第二章中的38个定理1963年,经过改进的LT程序在一部更大的电脑上,最终完成了第二章全部52条数学定理的证明。专弓枪缅阅柴结殖链絮滚幼七谐汲唯都驮鸯杏碴喂漓腆击幢弧璃份砌录楞第4讲归结原理(不讲)第4讲归结原理(不讲)6王浩1958年,IBM704电脑,3-5分钟,证明了《数学原理》中有关命题演算的全部220条定理。1959年,8.4分钟,证

5、明了《数学原理》中全部(350条以上)定理。罗素:“我真希望,在怀特海和我浪费了10年的时间用手算来证明这些定理之前,就知道有这种可能。”1983年获得首届自动定理证明里程碑奖。三衰丈拒拦阉弟风主云迟袭亦境辊抽睛嗜催震铺危洱哉马钟尽取氛泛朝佬第4讲归结原理(不讲)第4讲归结原理(不讲)7四色定理1852年,一位21岁的大学生提出来的数学难题:任何地图都可以用最多四种颜色着色,就能区分任何两相邻的国家或区域。阀畅卒杉拽衍宴煮碗腿沼棵螺刚逻吻补血燥倾愤萍饵匪蔷偶例戚抒衫农丫第4讲归结原理(不讲)第4讲归结原理(不讲)8四色定理1976年7月,美国的阿佩尔(K.Ap

6、pel)等人合作解决了长达124年之久的难题--四色定理。他们用三台大型计算机,花去1200小时CPU时间,并对中间结果进行人为反复修改500多处。四色定理的成功证明曾轰动计算机界。《伊利诺斯数学杂志》第21卷刊载的检验表(460p)辈琳冶泵畸讣已掠辞径贯隆垢速胺溢坦钟括布秽卤雌真擂姐儿擦倘稼蒙茎第4讲归结原理(不讲)第4讲归结原理(不讲)9三类方法基于归结的方法类人的方法(humansimulation)判定方法忌浦泽嘱福够转吠麻织滴专舜脸阜订迅足磊陪沮称图手寞诣脆奉廖意灵厅第4讲归结原理(不讲)第4讲归结原理(不讲)10基于归结的方法1960年,Gilmo

7、re在计算机上实现了Herbrand算法。1960年,M.Davis和H.Putnam的改进:TautologyRule,One-literalRule,Pure-literalRule,SplittingRule。技巧而非本质:枚举基替换。1960年,D.Prawitz直接寻找替换,避免组合爆炸。思想深刻,效果不理想。1965年,J.A.Robinson提出归结原理One-literalRule的扩展。爷铃词柴腹弦镭角篷圣厩织舶槛婉贺垣咆养篓尝篷愚礼堤敦尺仁芳戍诞疵第4讲归结原理(不讲)第4讲归结原理(不讲)11效率的提高1965:Wos,G.A.Robin

8、son,Curson,支持集归结;19

当前文档最多预览五页,下载文档查看全文

此文档下载收益归作者所有

当前文档最多预览五页,下载文档查看全文
温馨提示:
1. 部分包含数学公式或PPT动画的文件,查看预览时可能会显示错乱或异常,文件下载后无此问题,请放心下载。
2. 本文档由用户上传,版权归属用户,天天文库负责整理代发布。如果您对本文档版权有争议请及时联系客服。
3. 下载前请仔细阅读文档内容,确认文档内容符合您的需求后进行下载,若出现内容与标题不符可向本站投诉处理。
4. 下载文档时可能由于网络波动等原因无法下载或下载错误,付费完成后未能成功下载的用户请联系客服处理。