-
定理證明
鎖定
定理證明是指數學領域中對臆測的定理尋求一個證明,證明定理時,不僅需要有根據假設進行演繹的能力,而且需要有某些知覺的技巧,這是一項需要智能才能完成的任務。
- 中文名
- 定理證明
- 外文名
- theorem proving
- 領 域
- 數學領域
- 需 要
- 有根據假設進行演繹的能力
- 屬 性
- 一項需要智能才能完成的任務
定理證明主要發展
數學領域中對臆測的定理尋求一個證明,一直被認為是一項需要智能才能完成的任務。
證明定理時,不僅需要有根據假設進行演繹的能力,而且需要有某些知覺的技巧。例如數學家在求證一個定理時,會熟練地運用他豐富的專業知識,猜測應當先證明哪一個引理,精確判斷出已有的那些定理將其作用,並把主問題分解為若干問題,分別獨立進行求解。
因此人工智能研究中機器定理證明很早就受到注視。在人工智能的發展時期,1957年A.Newell、J.Shaw和H.Simon等人的心理學小組編制出一個稱為
[1]
邏輯理論機LT(The Logic Theory Machine)的數學定理證明程序,該程序證明了B.A.W.Russell和A.N.Whitehead的“數學原理”一書第二章的38個定理。並取得不少成果。
定理證明人類思維階段
(1) 先想出大致的解題計劃;
(2) 根據記憶中的公理定理和推理規則組織解題過程;
(3) 進行方法和目的分析,修正解題計劃。
由此可見定理證明在人工智能的發展中已取得不少成果。
定理證明重要性與意義
定理證明的研究在人工智能方法的發展中曾起到重要的作用,例如使用謂詞邏輯語言,其演繹過程的形式體系研究,幫助人們更清楚地理解推理過程的各個組成部分。
許多其他領域的問題,如醫療診斷信息檢索等也可以應用定理證明的方法,因此機器定理證明的研究具有普遍意義。
- 參考資料
-
- 1. 基於模糊邏輯理論的道路交通安全評價方法 .知網.2008-01-15[引用日期2016-12-04]