论文部分内容阅读
一、定理机器证明思想的产生与发展所谓定理的机器证明，是指使用计算机证明定理的成立，即把人证明定理的过程，通过一套符号体系加以形式化，变成一系列在计算机上自动实现的符号计算过程。其实质是把具有智能特点的推理演绎过程机械化。定理的机器证明是涉及人类智能问题的主要研究课题之一。从传统的手工证明到定理的机器证明，是现代数学思想方法的一次重大突破。机器证明大体上经历了这样一个过程：公理化代数化坐标化机械化。近代的机器证明思想由莱布尼兹首先提出，并直接导源于他的定理证明机械化设想。到19世纪末，希尔伯特等