自動化定理證明（也稱為 ATP 或自動演繹）是自動推理和數學邏輯的一個子領域，涉及通過計算機程序證明數學定理。 基于數學證明的自動推理是計算機科學發展的主要推動力。

雖然形式化邏輯的根源可以追溯到亞里士多德，但在 19 世紀末和 20 世紀初見證了現代邏輯和形式化數學的發展。 弗雷格的 Begriffsschrift (1879) 介紹了完整的命題演算和現代謂詞邏輯的本質。 他的 Foundations of Arithmetic 于 1884 年出版，用形式邏輯表達了（部分）數學。 羅素和懷特海在他們頗具影響力的《數學原理》中繼續采用這種方法，該書于 1910 年至 1913 年首次出版，并于 1927 年修訂了第二版。羅素和懷特海認為他們可以使用形式邏輯的公理和推理規則推導出所有數學真理，原則上 開放流程以實現自動化。 1920 年，Thoralf Skolem 簡化了 Leopold L?wenheim 先前的結果，得出了 L?wenheim-Skolem 定理，并在 1930 年提出了 Herbrand 宇宙的概念和 Herbrand 解釋，該解釋允許（不）滿足一階公式（因此 一個定理的有效性）被簡化為（可能是無限多的）命題可滿足性問題。

1929 年，Moj?esz Presburger 證明了加法和相等的自然數理論（現在以他的名義稱為 Presburger 算術）是可判定的，并給出了一種算法，可以確定語言中給定的句子是真還是假。然而，不久之后 庫爾特·哥德爾 (Kurt G?del) 發表了《數學原理及相關系統的形式上不可判定的命題》(On Formally Undecidable Propositions of Principia Mathematica and Related Systems) (1931)，表明在任何足夠強的公理系統中，都存在無法在系統中證明的真陳述。 這個話題在 1930 年代由 Alonzo Church 和 Alan Turing 進一步發展，他們一方面給出了兩個獨立但等價的可計算性定義，另一方面給出了不可判定問題的具體例子。

1954 年，Martin Davis 在新澤西州普林斯頓高等研究院為 JOHNNIAC 真空管計算機編寫了 Presburger 算法。 根據戴維斯的說法，它的偉大勝利是證明了兩個偶數之和是偶數。 更雄心勃勃的是 1956 年的邏輯理論機，這是一個用于數學原理命題邏輯的演繹系統，由 Allen Newell、Herbert A. Simon 和 J. C. Shaw 開發。 同樣在 JOHNNIAC 上運行的邏輯理論機從一小組命題公理和三個演繹規則構建證明：先決條件、（命題）變量替換，以及通過定義替換公式。 該系統使用啟發式指導，成功證明了《原理》前 52 個定理中的 38 個。

邏輯理論機的啟發式方法試圖模仿人類數學家，即使在原則上也不能保證每個有效定理都能找到證明。 相比之下，其他更系統的算法至少在理論上實現了一階邏輯的完整性。 最初的方法依賴于 Herbrand 和 Skolem 的結果，通過使用 Herbrand 宇宙中的項實例化變量，將一階公式轉換為連續更大的命題公式集。 然后可以使用多種方法檢查命題公式的不可滿足性。 Gilmore 的程序使用到析取范式的轉換，在這種范式中，公式的可滿足性是顯而易見的。

根據底層邏輯，決定公式有效性的問題從微不足道到不可能。 對于命題邏輯的常見情況，問題是可判定的但 co-NP-complete，因此一般證明任務只存在指數時間算法。 對于一階謂詞演算，哥德爾的完備性定理指出定理（可證明的陳述）恰好是邏輯上有效的格式正確的公式，因此識別有效公式是遞歸可枚舉的：給定無限資源，任何有效公式最終都可以被證明 . 然而，無效的公式（給定理論未包含的公式）并不總能被識別。