机器证明

使用计算机证明数学定理。机器证明的研究有试探法、判定法、证明算法和机器辅助法等方向。试探法是对所要证明的命题考虑若干种可能的证法，然后编程序逐一试验。判定法是在所要证明的命题所属的理论的判定问题获得解决的基础上，根据判定算法加以证明或否证。证明算法是将所要证明的命题表示为*谓词演算中的合式公式，然后，当此命题是定理时，可根据算法得出表示它的否定命题的公式是不可满足的（当命题不是定理时无结果）。机器辅助法是将证明中大量的繁琐工作交机器完成，因此是在机器的辅助下实现证明。