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