来源于:中国网
王浩是美国艺术与科学学院院士，英国科学院外藉院士和符号逻辑学协会会员．1983年在美国丹佛召开的，由人工智能国际联合会会议(Lnternational Joint Confernce on ArtificialinteIIigence)和美国数学会共同主办的，自动定理证明(Automated Theorem Proving)特别年会上，王浩被授予首届"里程碑奖"(Milestone Prize)，以表彰他在数学定理机械证明研究领域中所作的开创性贡献．提名时列举的主要贡献有：强调发展应用逻辑新分支--"推理分析"(inferential analysis)，其对于数理逻辑的依赖关系类似于数值分析(numericalanalysis)对于数学分析的依赖关系；坚持谓词演算和埃尔布朗(Herbrand)与根岑(Gentzen)形式化的基本作用；设计了证明程序，有效地证明了罗素与怀特海(Whitehead)的《数学原理》中带集式的谓词演算部分的350多条定理；第一个强调在埃尔布朗序列(Herbrand expansion)中预先消去无用项的算法的重要性；提出一些深思熟虑的谓词演算定理，可用作挑战性问题来帮助判断新的定理证明程序的效能．
与王浩先生交往二三事
今年是著名数理逻辑学家、哲学家、人工智能先驱王浩先生（1921～1995）去世十周年。十年前的夏天，很少买报的我不知为何买了一份《纽约时报》。翻到讣告版时，我被一幅吸着烟斗的中国人头像所吸引，仔细一看，竟然是王浩先生的照片。我清楚记得当时的感受：除了为这位大师的逝世遗憾之外，还有一种内疚感，为自己未能接受他的邀请去拜访他而感到内疚。
我是通过在纽约读书时的老师McNaughton教授与王浩先生认识的。一次上“定理证明”课，McNaughton提起王浩“一击七蝇”（Seven flies in one blow)的 传奇结果：利用早期的IBM计算机，仅用几分钟就自动证明了罗素花十年心血才在其名著《数学原理》中证明的220条命题，以至罗素闻后竟生“早知今日何必当初”的感叹。课后我问McNaughton，王浩到底是数学家还是哲学家？他没有回答我的问题，却告诉我当他还是哈佛大学的学生时，王浩就是哈佛哲学系的教授了。巧的是，McNaughton告诉我，王浩不久就要来学校参加会议，要我陪一下。
记不清是1989年还是1990年的春季，会议的名称也忘了，但记得是关于社会哲学与现代科技发展的讨论会。会议是在我校的工业创新中心大楼的二层演讲厅举办的，参加的人很少。休会期间，我带先生看了一下附近的校园，但多数时间是站在报告厅外面的阳台上，一边看着楼下绿绿的橄榄球场，一边随便聊天。当时自己丝毫没有同大师谈话的局促感，先生更是朴实得有些出人意料。他的穿着完全是一副刚刚从国内来美访问的学者派头，不知者根本就无法把他与近50年的西方生活经历联系到一起。
共34页
[1][2][3][4][5][6][7][8][9][10][11][12][13][14][15][16][17][18][19]
[20][21][22][23][24][25][26][27][28][29][30][31][32][33][34]
