摘要: 定理的机器证明是人工智能近代主攻的课题之一．早在十六世纪，人类就开始考虑这一问题，但由于历史条件的限制没能付诸实践．从本世纪六十年代以来，随着大型高速计算机的发展，人们继前辈之理论，集众人之精华研究出一个个精致的定理的机器证明方法，从而开创了这一学科的新纪元，为人类智力提供了从前梦想不到的源泉．