1.1 初期の試みとヒルベルトプログラム
自動定理証明の起源は、20世紀初頭の数理論理学の発展に遡る。ダフィット・ヒルベルトは、数学の全命題を有限の公理から機械的に導出可能とする「ヒルベルトプログラム」を提唱し、形式体系の完全性と決定可能性への期待を高めた。この構想は、後の計算理論と証明の自動化への基盤となったが、ゲーデルの不完全性定理により、完全な自動化には原理的限界があることが示された。それでも、限られた範囲での機械的証明の可能性は、後の研究の礎を築いた。
1.2 エルブランの貢献と導出原理
ジャック・エルブランは、1930年代にエルブランの定理を提案し、一階述語論理における証明の実行可能性に重要な洞察を与えた。彼の研究は、証明を有限回の操作で検証できる形に変換する方法を示し、後の自動証明における基本的手続きの原型となった。エルブランのアプローチは、導出原理の前駆として位置づけられる。
1.3 ロビンソンの導出原理とSAT
1965年、ジョン・アラン・ロビンソンは導出原理を発表し、一階述語論理における効率的な自動証明の実用的枠組みを確立した。導出原理は、単一化と組み合わせることで、矛盾検出を系統的に行う手法であり、SAT（充足可能性問題）解決の基盤ともなった。この発見は、自動定理証明を理論から実装可能な技術へと押し上げた。
2.1 論理体系
2.1.1 命題論理
命題論理は、真理値を取る命題変数と論理結合子（¬, ∧, ∨, →, ↔）からなる最も単純な形式論理である。各命題の真偽は真理値表で決定され、証明の対象はトートロジーや矛盾の判定に限られる。命題論理の決定可能性は高く、SATソルバーの基盤として広く利用される。
2.1.2 述語論理
述語論理は、命題論理に量化子（∀, ∃）と項・述語・関数記号を加えた拡張であり、数学的構造をより精密に表現できる。一階述語論理は半決定可能であり、多くの自動定理証明システムの基盤論理である。高階論理では関数や述語自体を量化でき、より表現力が高いが、自動証明は一層困難になる。
2.2 証明システム
2.2.1 自然演繹
自然演繹は、人間の自然な推論に近い形で証明を構成するシステムであり、各論理結合子に対する導入則と除去則から成る。証明は仮定を用いて導出されるため、直感的だが自動化には探索空間が大きくなる傾向がある。
2.2.2 シークエント計算
シークエント計算は、ゲルハルト・ゲンツェンによって導入された証明システムで、シークエント（前提列と結論列の対）を推論規則で変形する。カット除去定理により証明の正規化が保証され、自動証明における証明探索の基盤の一つとなっている。
2.3 決定可能性と半決定可能性
命題論理は決定可能であり、任意の論理式の充足可能性を有限時間で判定できる。一方、一階述語論理は半決定可能、すなわち恒真な式は有限時間で証明できるが、恒偽な式は停止しない可能性がある。この性質は、自動定理証明の探索戦略や停止条件に本質的な制約を与える。
3.1 導出原理と導出法
導出原理は、節形式（リテラルの選言）で表された論理式に対して二つの節から新たな節を導く規則である。具体的には、一方の節にリテラルL、他方の節に¬Lが含まれれば、それらを除去した残りのリテラルを結合した節を得る。導出法は、この原理を繰り返し適用し、空節（矛盾）を導くことで定理を証明する。ロビンソンの導出原理は、単一化により一階述語論理へ拡張された。
3.2 インスタンス化と単一化
3.2.1 単一化アルゴリズム
単一化は、二つの項（またはリテラル）を同一にする代入（置換）を求めるアルゴリズムである。一階単一化は、一意な最汎単一化子を効率よく計算できる。通常は、差異対を解消しながら代入を合成する逐次的手法が用いられる。
3.2.2 最汎単一化子
最汎単一化子（most general unifier, mgu）は、与えられた二つの項を等しくする代入の中で最も一般的なもの（他の代入がその代入を具体化したもの）を指す。導出原理では、mguを用いることで最小限の具体化で導出が可能となり、証明探索の効率が向上する。
3.3 ヒューリスティック探索
3.3.1 深さ優先探索
深さ優先探索は、導出の木を優先的に深く探索する戦略である。スタックを用いて実装され、メモリ消費が少ないが、無限ループや無駄な枝に陥りやすい。自動証明器では、深さ制限や枝刈りと併用される。
3.3.2 幅優先探索
幅優先探索は、同一深さの節をすべて優先し、徐々に深さを増やす戦略である。完全性を持つが、証明空間が爆発的に広がる問題では実用的でない場合が多い。主に、探索空間が狭い問題や初期のデバッグに用いられる。
3.3.3 最良優先探索
最良優先探索は、ヒューリスティック関数で各節の「有望度」を評価し、最も有望な節から優先的に導出を進める。例えば、節の長さやリテラル数に基づく重み付けが一般的で、多くの高効率な証明器で採用されている。探索の完全性と効率のバランスを取る工夫が必要である。
3.4 超導出とバリエーション
超導出（hyperresolution）は、複数の前提節から一度に導出を行う技法であり、特に正リテラル（または負リテラル）のみの導出に特化することで探索を効率化する。他にも、パラモジュレーション（等号推論）、意味導出、線形導出など、様々なバリエーションが開発され、特定のクラスの問題に対して効果を発揮する。
4.1 古典的な証明器
4.1.1 Otter
Otterは、1980年代にアーゴンヌ国立研究所で開発された一階述語論理の自動証明器であり、導出原理と重み付けヒューリスティックを中核とする。多くの数学定理の証明（例えば、ロビンス代数問題）に成功し、自動証明コミュニティに大きな影響を与えた。現在も教育・研究で利用されている。
4.1.2 E prover
E proverは、高速な一階述語論理の証明器で、導出原理に加えてインスタンス化や等号処理に優れた実装を持つ。CASC（自動定理証明競技会）で高い成績を収め、特にSATと組み合わせたSMTソルバーへの組み込みにも用いられる。オープンソースとして公開されている。
4.2 高階論理対応システム
4.2.1 Isabelle
Isabelleは、高階論理を扱う対話的定理証明支援システムであり、自動化機能（自動証明器、SMTソルバーとの連携）も備える。証明は人間が戦略を指示しながら進めるスタイルが基本で、証明の可読性と信頼性が重視される。多くの数学・検証プロジェクトで実績がある。
4.2.2 Coq
Coqは、依存型を用いた高階論理の証明支援システムで、証明を関数型プログラムとして記述できる。自動証明のためのタクティク（自動証明コマンド）や外部証明器との統合も完備し、ソフトウェアの形式検証や数学の定理証明（例：四色定理の証明の一部分）に広く使用される。
4.3 SAT/SMTソルバーとの融合
4.3.1 MiniSat
MiniSatは、高速かつコンパクトなSATソルバーの実装であり、CDCL（Conflict-Driven Clause Learning）アルゴリズムを採用する。多くの派生実装を生み出し、自動定理証明における命題論理の効率的な解法として基盤を提供している。教育用としてもよく使われる。
4.3.2 Z3
Z3は、Microsoft Researchが開発した高効率なSMTソルバーで、一階述語論理や算術、配列、ビットベクトルなど多様な理論を組み合わせた充足可能性判定を行う。自動定理証明の文脈では、他の証明器と連携してサブ問題を解決したり、式の妥当性検証に利用される。APIが充実しており、検証ツールのバックエンドとして普及している。
5.1 数学定理の証明
5.1.1 四色定理の証明
四色定理は、1976年にアッペルとハーケンがコンピュータ支援により証明したことで知られるが、その後、Coqなどの証明支援系で完全に形式化・自動検証された。これにより、コンピュータによる大規模数学証明の可能性が示された。
5.1.2 ケプラー予想の検証
ケプラー予想（球充填問題）は、トーマス・ヘイルズらのグループによってコンピュータプログラムを用いて証明された。自動定理証明技術は、この証明の形式化と検証に一部利用され、FlyspeckプロジェクトでCoqを用いて完全に検証された。
5.2 ソフトウェア検証
ソフトウェアのバグ発見や正当性保証に自動定理証明が活用される。例えば、バッファオーバーフローやヌルポインタ参照などの脆弱性を、ソースコードから論理式に変換し、証明器で検証する手法が研究・実用化されている。静的解析ツールやモデル検査と連携するケースが多い。
5.3 ハードウェア検証
ハードウェア設計（特にFPGAやASIC）の論理回路が仕様を満たすかどうかを、SAT/SMTソルバーや自動証明器を用いて検証する。命題論理の等価性検証や、バイナリレベルでの振る舞い検証が代表的であり、製品の信頼性向上に寄与する。
5.4 人工知能と推論
自動定理証明は、知識表現やエキスパートシステムにおける推論エンジンとして応用される。特に、一階述語論理を用いた質問応答やプランニング、自動推論の研究分野で基盤技術となっている。近年は、機械学習と組み合わせた新たな推論手法も模索されている。
6.1 証明の複雑性
自動定理証明は、問題の大きさに対して指数的な探索空間を持つため、実用的な時間内で解ける問題は限られる。特に、一階述語論理の半決定可能性は、証明が存在しても停止しない可能性がある。効率的なヒューリスティックや分割統治の手法が必要である。
6.2 ヒューマン・マシン協調
完全自動化の限界から、人間が証明戦略の指針を与える対話的証明支援が現実的な手法として広く使われている。証明の進行状況を人間が把握し、適切な補題や戦略を提示することで、複雑な証明が可能になる。この協調の効率化が今後の課題である。
6.3 不完全性定理と自動証明の限界
ゲーデルの不完全性定理は、十分強力な形式体系（例えばペアノ算術）において、証明も反証もできない文が存在することを示す。これにより、自動定理証明がすべての数学的真理をカバーすることは原理的に不可能である。ただし、実際の応用では、多くの有用な定理が形式化可能であり、限界を認識した上で活用される。