定理机器证明

---

指数学定理证明过程的机械化。

数学这种脑力劳动有两种形式：计算与证明。计算过程虽然繁琐，但却是简单的，计算规则是明确的，过程是呆板的，而证明过程却不然，它依赖于直觉、洞察、经验和一些模糊的不易模仿的规则来进行，因此一个证明过程能表现出它的灵活、美妙的特性。产生出这种区别的原因在于：计算过程是可以机械化的；而证明过程还没有能机械化。如何使数学定理证明的过程机械化，这就是定理机器证明研究的主要内容。17世纪大数学家莱布尼兹就有了数学定理证明机械化的设想，这个设想使莱布尼兹创立了数理逻辑这门学科。直到20世纪，由于数理逻辑的发展，尤其是电子计算机的产生，才使得这一设想有了实现的可能。定理机器证明在20世纪50～60年代非常活跃，主要有以下几种研究途径：自然推导法：这种方法是模拟人在证明定理时的思维过程。奠基性工作有1956年纽厄尔(Newell)、萧(Shaw)、西蒙(Simon)做出的逻辑理论家系统、盖林特(Gelernter)做出的初等几何证明机。

对一类问题找判定算法：著名的工作有1951年泰斯基(Tarski)和1976年吴文俊教授给出的初等几何及初等代数的判定方法。归纳方法：1965年由罗宾逊(Robinson)提出的一阶逻辑的半可判定算法。定理机器证明是人工智能中重要课题，它的成果可以应用于问题解答、自然语言理解、程序正确性证明和自动程序设计等方面。