1956年夏天举行的达德茅斯研讨会,被认为是人工智能作为一门
独立学科正式诞生的标志.这次研讨会聚集了来自数学、信息科学、
心理学、神经生理学和计算机科学等不同领域的领导者,包括Minsky,
Rochester,Shanon,Samuel,Moore,Simon,Newell,Selfirdge,Solonionff
和Mccarthy等.其中,Miusky,Mccarthy,Newell和Simon后来被认为
是美国人工智能界的“四大领袖”.与会者从不同角度搜索了使机器具有智能
的途径和方式,并决定用“人工智能”(Artificial Intelligence)一词来概括
这一新的研究方向.达德茅斯研讨会开创了人工智能的第一个发展时期.在这个
时期里,研究者们展开了一系列开创性工作,并取得了引人注目的成果.
会后不久,Newell,Shaw和Simon完成了一个自动证明数学定理的计算机程序Logic Theorist
(此前Martin和Davis曾编制了一个算术定理的证明程序,但未发表),证明了《数学
原理》第二章中的38条定理,由此开创了人工智能智能中“自动定理证明”这一分
支.1958年,美籍逻辑学家王浩在自动定理证明中取得的重要进展.他的程序在IBM704
计算机上用不到5分钟的时间证明了《数学原理》中“命题演算”的全部220条定理.1959年, 数据挖掘工具
王浩的改进程序用8．4分钟证明了上述220条定理及书中带等词的谓词演算的绝大部分定理.
1983年,美国数学学会将自动定理证明的第一个“里程碑奖”授予王浩,以表彰他的杰出贡献
(自动定理证明的“里程碑奖”每25年评选一次,由此可见其份量).受王浩工作的鼓舞,自动
定理证明的研究形成一股热潮.比如,Slagle的符号积分程序SAINT经测试已达到了大学生的
积分演算水准;而Mosis的SIN程序的效率比SAINT提高了约三倍,被认为达到了专家水平.
自动定理证明的理论价值和应用范围并不局限于数学领域.事实上,很多问题可以转化为定理
证明问题,或者与定理证明有关.可以认为,自动定理证明的核心问题是自动推理,
而推理在人的智能行为中起普遍性的重要作用.基于这一看法,在自动定理证明的
基础上进一步研究通用问题求解,是一个值得探索的课题.从1957年开始,Newell,
Shaw和Simon等人着手研究不依赖与具体领域的通用解题程序,称之为GPS,它是在
Logic Theorist的基础上发展起来的,虽然后来的实践表明,GPS作为一个独立的求解程序
的能力是有限的,但在GPS中发展起来的技术(yo means-ends分析）对人工智能的发展有
重要意义． 数据挖掘交友
|
