摘要: 两年一度的J.McCarthy奖是为表彰在程序验证领域的杰出工作而设立的。首次奖是根据最近五年在该领域发表的研究工作评定的。美国德克萨斯大学的R.S.Boyer和J S.Moore被评选为首次获奖人。Boyer和Moore从七十年代就合作研究定理证明和程序验证。他们的主要成就是成功地发展了一种可实现高效率的定理证明系统的严谨的逻辑。这种逻辑特别强调了归纳法的使用以表现程序共有的属性。他们的系统是现今最有效的定理证明系统之一。该系统使用启发式来加强其自动定理证明的功能,并允许用户通过人权交换来推导不能由机器完全自动完成的证明。他们还扩充了该系统,使之包括一个FORTRAN验证条件产生程序,使该系统可以处理FORTRAN这