定理證明

數學領域中對臆測的定理尋求一個證明，一直被認為是一項需要智能才能完成的任務。

證明定理時，不僅需要有根據假設進行演繹的能力，而且需要有某些知覺的技巧。例如數學家在求證一個定理時，會熟練地運用他豐富的專業知識，猜測應當先證明哪一個引理，精確判斷出已有的那些定理將其作用，並把主問題分解為若干問題，分別獨立進行求解。

因此人工智能研究中機器定理證明很早就受到注視。在人工智能的發展時期，1957年A.Newell、J.Shaw和H.Simon等人的心理學小組編制出一個稱為 ^[1]  邏輯理論機LT（The Logic Theory Machine）的數學定理證明程序，該程序證明了B.A.W.Russell和A.N.Whitehead的“數學原理”一書第二章的38個定理。並取得不少成果。

（1） 先想出大致的解題計劃；

（2） 根據記憶中的公理定理和推理規則組織解題過程；

（3） 進行方法和目的分析，修正解題計劃。

由此可見定理證明在人工智能的發展中已取得不少成果。

定理證明的研究在人工智能方法的發展中曾起到重要的作用，例如使用謂詞邏輯語言，其演繹過程的形式體系研究，幫助人們更清楚地理解推理過程的各個組成部分。

許多其他領域的問題，如醫療診斷信息檢索等也可以應用定理證明的方法，因此機器定理證明的研究具有普遍意義。