このページは 述語論理・一階論理を用いた定理証明 と、それを支える理論の歴史を、できるだけやさしい言葉でまとめたノートです。ルールベースモデル全体の史 より範囲を狭くし、形式化と機械化の系譜に焦点を当てています（数学基礎論の厳密な年表ではありません）。
近代論理から「機械で証明する」へ
その前に：数理論理学とは全部「機械証明」ではない
数理論理学はもともと 数学の一分野で、矛盾やパラドックスを慎重に扱い、推論や数学の「土台」を 記号と決まった規則 で語ろうという流れがあります。「AI の学問」だけではありませんし、単に そういう式が機械でチェックできるだけが目的とも限りません。
それでも後のコンピュータ時代とつながる理由
だいたい 19 世紀末から 20 世紀前半にかけて、Frege、Russell、Hilbert らの流れで進んだのは、ざっくり次のイメージです。
- 文章の「なんとなく正しそう」だけでなく、どんな記号の並びが式か、どんなときだけ次の式へ進んでよいかを、可能な限り はっきり書く（形式化する）。
- そうすると、証明は 許された変形の列として見える。各ステップがルールに合っているかは、意味に頼らず 形だけでも照合しやすい。
つまり 「数理論理学＝機械的検証そのもの」ではなく、あとから計算機が得意とする「記号にしたがった手続き」という見方の下地が、この時期に固まってきた、と読むと近いです。
ヒルベルトまわりの「数学を形式系に落とし、手続きで検査する」という夢は、その後 ゲーデルの不完全性定理などで「そんなに単純にはいかない」ことがはっきりしましたが、形式化して検査するという発想自体は 計算機科学・自動証明へつながっています。
自動定理証明の転機（1960 年代）
J. A. Robinson の 解消原理（resolution, 1965 年） は、自動定理証明研究の大きな転機として繰り返し挙げられます。探索空間は依然として巨大ですが、一つの統一的な推論ルールとして扱いやすくなり、実装研究が活発化しました。
AI との接点
記号処理 AI の文脈では、定理証明は 推論エンジンの原型の一つでした。一方で、現実の数学やソフトウェアの規模では 完全自動は難しく、ヒューリスティック、対話的証明、高階や型理論への拡張など、人と協働する証明へと発展しています。
ロジックプログラミング（../logic-programming/history.md）は、同じ論理の道具を 計算パラダイムとして再解釈した系譜です。
いまの位置づけ
ハードウェア・ソフトウェアの検証、SMT ソルバ、対話型証明系（Coq、Isabelle など）など、安全クリティカルな領域で重要性は高いままです。機械学習全盛のいまも、「なぜ正しいか」を形式化して示す需要は別軸で伸びています。