中的一個證明例子]]
自動化定理證明（，簡稱ATP）是自動推理（AR）體系中發展最成熟的子領域，其目的是使用電子計算機程序來進行數學定理的證明。對於不同的公理系統，自動定理證明器能夠推論出一個定理在此系統下是正確的、不可證明的還是錯誤的。
邏輯基礎
形式化邏輯的根源可追溯至亞里士多德，但現代邏輯和形式化數學的發展主要在19世紀末至20世紀初。戈特洛布·弗雷格的《概念文字》（1879年）引入了完備的命題邏輯和本質上是現代謂詞邏輯的系統。伯特蘭·羅素和阿爾弗雷德·諾思·懷特黑德在1910–1913年出版的《數學原理》中延續了這一方向，試圖從形式邏輯的公理和推理規則推導出所有數學真理，從原則上開啟了自動化的可能。
1920年，托拉爾夫·斯科倫簡化了利奧波德·勒文海姆先前的結果，提出了勒文海姆–斯科倫定理；1930年，雅克·埃爾布朗的工作引入了埃爾布朗宇宙和埃爾布朗解釋的概念，將一階公式的（不）可滿足性歸約為（可能無限的）命題可滿足性問題。1929年，莫伊塞斯·普雷斯布格證明，帶有加法和等式的自然數一階理論（今稱普雷斯布格算術）是可判定的，並給出了判定算法。
然而，庫爾特·哥德爾在1931年發表的《論《數學原理》及相關體系的形式不可判定命題》表明，在任何足夠強的公理化系統中，都存在真而不可證的命題（哥德爾不完備定理）。這一主題在1930年代由阿隆佐·邱奇和艾倫·圖靈進一步發展，他們分別給出了可計算性的等價定義，並提供了不可判定問題的具體例證。
早期實現
1954年，馬丁·戴維斯在普林斯頓高等研究院的JOHNNIAC真空管計算機上實現了普雷斯布格的算法。據戴維斯所說，其“最大的成功是證明了兩個偶數之和為偶數”。更為雄心勃勃的是1956年的邏輯理論家程序，由艾倫·紐厄爾、赫伯特·西蒙和克利夫·肖開發，用於證明《數學原理》中的命題邏輯定理。該程序使用啟發式引導，成功證明了《數學原理》第二章52條定理中的38條。
可判定性與局限
公式有效性的判定問題因底層邏輯的不同而從平凡到不可解不等。命題邏輯是可判定的，但屬於co-NP完全問題，一般認為僅存在指數時間算法。對於一階謂詞演算，哥德爾完備性定理指出有效公式恰恰是可證明的公式，因此有效公式是可計算枚舉的：在無限資源下，任何有效公式最終都能被證明。然而，_無效_公式（不被理論蘊涵的公式）並非總能被識別。
上述結論適用於一階理論（如皮亞諾算術）。然而，對於一階理論描述的特定模型，某些語句可能為真但在所用理論中不可判定。哥德爾不完備定理表明，任何其公理對自然數為真的一致理論都無法證明所有對自然數為真的一階語句。
應用
自動定理證明的商業應用主要集中在集成電路設計與驗證領域。自奔騰FDIV缺陷之後，現代微處理器的複雜浮點運算單元在設計時受到了額外的審查。AMD、英特爾等公司使用自動定理證明來驗證除法及其他運算的正確實現。其他用途包括程序綜合（構造滿足形式化規格的程序）以及與證明助手（如Isabelle/HOL）的集成。定理證明器也被應用於自然語言處理和形式語義學領域，用於分析話語表示。
基準測試與系統
自動定理證明系統的質量受益於大規模標準基準測試庫——TPTP（Thousands of Problems for Theorem Provers）問題庫。此外，自動演繹會議（CADE）每年舉辦CADE ATP系統競賽（CASC），選用TPTP庫中的題目進行評比。重要的ATP系統包括：E（基於純等式演算的高性能證明器）、Vampire（自2001年以來多次贏得CASC冠軍）、SPASS（一階邏輯帶等式證明器）、Prover9（接替Otter的證明器）以及Z3（兼作SMT求解器）。
參見
- 自動推理
- 電腦協助證明
- 形式化驗證
參考文獻
评论 (0)