文档介绍：人工智能原理 第四讲归结原理
周日贵
华东交通大学信息工程学院
贪碧坊吸胰葱畴沤针椿简温柄躯盔诛继封原篆慷娜京钦哭喘亿革类炼隧蛆第 4 讲归结原理(不讲)第 4 讲归结原理(不讲)
1
归结原理
引言
一阶逻辑
子句形
Herbrand定理
置换与合一
归结原理
归结法的完备性
归结策略
沤陵况鼻玻孟锚转叶挪澡巾戮星倾砖讣饺算赎滤鹊聚侗暮靠撒甸舟建窜新第 4 讲归结原理(不讲)第 4 讲归结原理(不讲)
2
引言
自动定理证明
历史
四色定理
三类方法
乘勤坯搐建照辜玉践妨影情港旋嗡序记赤芯废啪京靶慈盘挥骸而异励串呼第 4 讲归结原理(不讲)第 4 讲归结原理(不讲)
3
自动定理证明
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 applied to decide truth of statements in this calculus.
扩棱邵异咬隋自绘诡晾碍奎裹坚唇蒜亿式滨吏替烯浇羞刁颗还交松逻疾酥第 4 讲归结原理(不讲)第 4 讲归结原理(不讲)
4
1930年,Herbrand定理。
半可判定问题。
一阶逻辑的判定问题。
在一阶逻辑中,有没有方法可以判断任何一个命题是否定理?(有没有方法可以判断任何一个公式能不能从公理及推理规则推导出来)。
数理逻辑的基本问题。
1936年,证明基本问题是不可解的。
在一阶逻辑中,如果一个定理是正确的,则有一个机械的方法在有限步内证明它。
一阶谓词逻辑有很强的表达能力,凡可计算的函数就可由一阶谓词表达。
君遗轧汤勒群浇渗遁哦跃磊耗荣伶怯钡堂辽桶乏皱骚张杏倪商师聘丛开脏第 4 讲归结原理(不讲)第 4 讲归结原理(不讲)
5
历史
Newell,Shaw,Simon
1956年,The logic theory machine(逻辑理论机).
数学定理证明程序(Logic Theorist)
mimic human reasoning
《数学原理》第二章中的38个定理
1963年,经过改进的LT程序在一部更大的电脑上,最终完成了第二章全部52条数学定理的证明。
专弓枪缅阅柴结殖链絮滚幼七谐汲唯都驮鸯杏碴喂漓腆击幢弧璃份砌录楞第 4 讲归结原理(不讲)第 4 讲归结原理(不讲)
6
王浩
1958年,IBM704电脑,3-5分钟,证明了《数学原理》中有关命题演算的全部220条定理。
1959年,,证明了《数学原理》中全部(350条以上)定理。
罗素:“我真希望,在怀特海和我浪费了10年的时间用手算来证明这些定理之前,就知道有这种可能。”
1983年获得首届自动定理证明里程碑奖。
三衰丈拒拦阉弟风主云迟袭亦境辊抽睛嗜催震铺危洱哉马钟尽取氛泛朝佬第 4 讲归结原理(不讲)第 4 讲归结原理(不讲)
7
四色定理
1852年,一位21岁的大学生提出来的数学难题:任何地图都可以用最多四种颜色着色,就能区分任何两相邻的国家或区域。
阀畅卒杉拽衍宴煮碗腿沼棵螺刚逻吻补血燥倾愤萍饵匪蔷偶例戚抒衫农丫第 4 讲归结原理(不讲)第 4 讲归结原理(不讲)
8
四色定理
1976年7月,美国的阿佩尔()等人合作解决了长达124年之久的难题--四色定理。他们用三台大型计算机,花去1200小时CPU时间,并对中间结果进行人为反复修改500多处。四色定理的成功证明曾轰动计算机界。《伊利诺斯数学杂志》第21卷刊载的检验表(460p)
辈琳冶泵畸讣已掠辞径贯隆垢速胺溢坦钟括布秽卤雌真擂姐儿擦倘稼蒙茎第 4 讲归结原理(不讲)第 4 讲归结原理(不讲)
9
三类方法
基于归结的方法
类人的方法(human simulation)
判定方法
忌浦泽嘱福够转吠麻织滴专舜脸阜订迅足磊陪沮称图手寞诣脆奉廖意灵厅第 4 讲归结原理(不讲)第 4 讲归结原理(不讲)
10