機器證明
機

機器證明　　　jī qì zhèng míng

使用計算機證明數學定理。機器證明的研究有試探法、判定法、證明算法和機器輔助法等方向。試探法是對所要證明的命題考慮若干種可能的證法，然后編程序逐一試驗。判定法是在所要證明的命題所屬的理論的判定問題獲得解決的基礎上，根據判定算法加以證明或否證。證明算法是將所要證明的命題表示為*謂詞演算中的合式公式，然后，當此命題是定理時，可根據算法得出表示它的否定命題的公式是不可滿足的（當命題不是定理時無結果）。機器輔助法是將證明中大量的繁瑣工作交機器完成，因此是在機器的輔助下實現(xiàn)證明。