定理證明

定理證明是指數學領域中對臆測的定理尋求一個證明，證明定理時，不僅需要有根據假設進行演繹的能力，而且需要有某些知覺的技巧，這是一項需要智慧型才能完成的任務。

基本介紹

• 中文名：定理證明
• 外文名：theorem proving
• 領域：數學領域
• 需要：有根據假設進行演繹的能力
• 屬性：一項需要智慧型才能完成的任務

主要發展

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

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

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

人類思維階段

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

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

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

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

重要性與意義

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

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