达了大学生的积分演算水准;而 Mosis 的 SIN 程序的效率比 SAINT 提
高了约三倍,被认为到达了专家水平。
自动定理证明的理论价值和应用围并不局限于数学领域。事实上,
很多问题可以转化为定理证明问题,或者与定理证明有关。可以认为,
自动定理证明的核心问题是自动推理,而推理在人的智能行为中起普
遍性的重要作用。基于这一看法,在自动定理证明的根底上进一步研
究通用问题求解,是一个值得探索的课题。从 1957 年开场,Newell,
Shaw 和 Simon 等人着手研究不依赖于具体领域的通用解题程序,称
之为 GPS,它是在 Logic Theorist 的根底上开展起来的,虽然后来的
实践说明,GPS 作为一个独立的求解程序,其能力是有限的,但在 GPS
中开展起来的技术对人工智能的开展有重要意义.
人工智能早期研究给人的深刻印象是博羿,1956 年,Samnel 研
制了一个西洋跳棋程序,该程序“天生〞下跳棋水平很低,远远不是
Samuel 的对手。但它有学习能力,能从棋谱中学习,也能在实践中总
结提高。经过三年的“学习〞,该程序与 1959 年打败了 Samuel;又经
过三年,打败了美国一个州的冠军。值得注意的是,虽然下棋至多只
能算是一项体育运动,下棋的程序似乎只是一种游戏程序,但 Samuel
工作的意义十分重大:它同时刺激了“搜索〞和“机器学习〞这两个
人工智能重要领域的开展。
与自动定理证明的研究意义不限于数学一样,搜索的研究意义也
不限于博弈。根据认知心理学的信息处理学派的观点,人类思维过程
的很大一局部可以抽象为从问题的初始状态经中间状态到达终止状