机器证明是人工智能的一个重要研究领域,人工智能作为一门新兴学科,是自然科学与社会科学的交叉学科,是逻辑学、思维科学、生理学、心理学、计算机科学、电子学、语言学、教育学等多学科相互渗透的结果.20世纪以来,数理逻辑的发展和完善、计算机科学的产生和发展为人工智能的产生提供了基础.机器证明是把人类证明定理的过程通过一套符号体系加以形式化,变成一系列能在计算机上自动实现的符号演算过程,即把具有智能特点的推理演算过程机械化.纽厄尔、西蒙和肖三人提出的"逻辑理论家"程序开创了定理机器证明这一分支,著名逻辑学家、计算机科学家王浩也为这一领域的发展做出了突出贡献,成为定理机器证明的开创者之一.王浩于1958年设计了三个逻辑定理证明程序,程序Ⅰ给出了命题演算的一个证明判定程序,它能根据命题是否是定理打印出一个证明或一个反证;程序Ⅱ用于处理具有最小范围形式的AE谓词演算,这个程序指令机器从基本符号形成自己的关于命题演算的命题并选出重要的定理;程序Ⅲ是为带等词的整个谓词演算所编写的大一点的程序的一部分.王浩用这三个程序在计算机上用了不到9分钟时间就证明了怀特海和罗素合著的《数学原理》中一阶逻辑的全部定理(将近400条),为此他获得了1983年国际人工智能联合会颁发的第一届"数学定理机械证明里程碑奖".王浩的贡献不仅在于他在机器上用相当快的速度证明了这些定理,而且还在于他表明了机器在一个广泛的研究和发展领域中的巨大潜力.他的一些有关机器证明的精辟论点,诸如以量的复杂取代质的困难,以及基础机证与特例机证应有区别等等,也是发人深思和使人深受启迪的.王浩还第一次明确提出了"走向数学的机械化"的口号,促进了数学基础研究的发展.