定理机器证明思想的产生与发展

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