自動定理証明（英: automated theorem proving, ATP）とは、自動推論 (AR) の中でも最も成功している分野であり、コンピュータプログラムによって数学的定理に対する証明を発見すること。ベースとなる論理によって、定理の妥当性を決定する問題は簡単なものから不可能なものまで様々である。
歴史
論理学的背景

論理学の起源はアリストテレスまで遡るが、現代的数理論理学は19世紀末から20世紀初頭に発展した。フレーゲの『概念記法』(1879) が完全な命題論理と一階述語論理の基本的なものを導入[1]。同じくフレーゲの『算術の基礎』(1884)[2]でも、形式論理の数学（の一部）を説明している。この流れを受け継いだのがラッセルとホワイトヘッドの『プリンキピア・マテマティカ』で、初版は1910年から1913年に出版され[3]、1927年に第2版が出ている[4]。ラッセルとホワイトヘッドは、公理と形式論理の推論規則からあらゆる数学的真理が導き出せると考え、証明自動化への道を拓いた。1920年、トアルフ・スコーレムはレオポールト・レーヴェンハイム（英語版）の成果を単純化したレーヴェンハイム-スコーレムの定理をもたらし、1930年にはエルブラン領域とエルブラン解釈により、一階の論理式の充足（不）可能性（および定理の妥当性）を命題論理の充足可能性問題に還元できることが示された[5]。

1929年、Moj?esz Presburger はプレスブルガー算術（加法と等号のある自然数の理論）が決定可能であり、その言語内の任意の文の真偽を判定できるアルゴリズムを示した[6][7]。しかしその直後、クルト・ゲーデルが Uber formal unentscheidbare Satze der Principia Mathematica und verwandter Systeme I (1931) を発表し、十分に強力な公理系はその体系内で証明も反証もできない文を含みうることを示した。1930年代にこの課題を研究したのがアロンゾ・チャーチとアラン・チューリングで、それぞれ独自に等価な計算可能性の定義を与え、決定不能な具体例も示した。
最初の実装

第二次世界大戦後、第一世代のコンピュータが登場。1954年、マーチン・デービス（英語版）がプリンストン高等研究所にて真空管コンピュータJOHNNIAC（英語版）上にプレスブルガーのアルゴリズムを実装した。デービスによれば「2つの偶数の総和も偶数であることを証明するという大きな成果があった」という[7][8]。さらに野心的な試みとして Logic Theorist がある。これはアレン・ニューウェルとハーバート・サイモンとクリフ・ショーが開発したもので、『プリンキピア・マテマティカ』の命題論理を対象とした推論システムだった。こちらもJOHANNIAC上で動作し、命題論理の少数の公理と推論規則（モーダスポネンス、命題変数の置換など）から証明を構築した。ヒューリスティックによる誘導を使っており、『プリンキピア・マテマティカ』の52の定理のうち38の証明に成功した[7]。

Logic Theoristのヒューリスティックとは人間の数学者のエミュレートを試みることであり、妥当な定理すべてについて証明できることを保証できなかった。対照的に、より体系的なアルゴリズムで（少なくとも理論上は）一階述語論理の完全性を達成できている。初期の手法ではエルブランとスコーレムの成果に基づき、一階述語論理の論理式を複数の命題論理の論理式に変換していた。そして、いくつかの技法で命題論理式の充足不可能性をチェックする。ギルモアのアルゴリズムは加法標準形に変換することで充足可能性を判定しやすくしていた[7][9]。
問題の決定可能性

使用する論理によって、論理式の妥当性の判定は自明なものから不可能なものまで様々である。命題論理の多くの問題では、定理は決定可能だがco-NP完全問題であり、汎用的な証明には指数時間アルゴリズムしかないと考えられている。一階述語論理では、完全性定理より妥当な論理式は証明可能であり、その逆も成り立つから、妥当な論理式の全体は再帰的に枚挙可能である。したがって、妥当な論理式の証明を機械的に探索することはできる。

妥当でない文、すなわち与えられた定理から意味論的に導かれない式は認識可能とは限らない。さらにゲーデルの不完全性定理によれば、ある程度の算術を含む無矛盾な体系は本質的不完全であり、本質的不完全な体系は本質的決定不可能であるから、とくに決定不可能である。