- 現代人工智能技術
- 李遠征 曾志剛等編著
- 560字
- 2024-06-26 16:50:29
1.4.1 自動定理證明
自動定理證明是用機器來幫助證明數學或邏輯中的一些結論是否正確。這是人工智能一個很重要的研究方向,也是讓機器自我推理的關鍵技術。
自動定理證明的做法是把要證明的結論寫成一種邏輯語言,然后讓機器按照一些規則和步驟來找到證明或者反駁。
自動定理證明有兩種主要方法:一種是完全交給機器去做,用到了SAT、SMT、一階定理證明等算法;另一種是需要人和機器合作,人來提供一些提示和指導。
自動定理證明在很多領域都有用處,比如數學、計算機科學、軟件工程、形式化方法等。它可以幫人們發現新的數學結論,檢查已經證過的結論是否有錯,保證程序和系統能正常和安全地運行等。
自動定理證明是人工智能里最早研究并成功應用的一個方向,也是推動人工智能發展的一個重要力量。其實,不光是數學里面的結論,像醫療診斷、信息檢索、問題求解等很多其他領域的問題,也可以變成定理證明問題。
定理證明就是要證明從前提P出發能得到結論Q。但是,這樣直接證明一般很難。常用的方法是反證。在這方面,海伯倫和魯濱遜兩位學者都做了很有價值的研究,提出了相應的理論和方法,為自動定理證明打下了理論基礎。特別是魯濱遜提出的歸結原理讓定理證明能在機器上實現,對機器推理有了重大貢獻。我國吳文俊院士提出并實現的“吳氏方法”,可以讓計算機證明幾何定理,是機器定理證明領域的一項里程碑式成果。