自動推論（じどうすいろん、Automated Reasoning）は計算機科学と数理論理学の一分野であり、推論の様々な側面を理解することでコンピュータによる完全（あるいはほぼ完全）自動な推論を行うソフトウェアを開発することを目的とする。人工知能研究の一部と考えられるが、理論計算機科学や哲学とも深い関係がある。
自動推論のなかでも最も研究が進んでいるのは、自動定理証明（および完全自動ではないがより現実的な対話型定理証明
（英語版））と自動定理検証（英語版）（固定の前提条件下での推論と見なすことができる）であるが、他にも類推、帰納、アブダクションによる推論の研究も盛んである。他の重要なトピックとしては、不確かさのある状況での推論と非単調推論である。不確かさに関する研究では論証（argumentation）が重要である。それはすなわち、標準的な自動推論へのさらなる極小性と一貫性の適用である。John Pollock の Oscar システムは単なる自動定理証明機よりも自動論証システムといえるものである。自動推論のツールや手法としては、古典的論理学や代数学があるが、他にもファジィ論理、ベイズ推定、最大エントロピー原理に基づく推論、その他のあまり形式的でない技法などがある。 数理論理学の発展は自動推論の分野で大きな役割を果たし、自動推論自体も人工知能の発展に寄与した。形式的証明 (formal proof) は、すべての論理的結論を基本的な数学の公理にまで遡ってチェックした証明である。すべての中間的な論理段階が示され、例外はない。直観から論理への変換が普通であっても、直観にたよることはない。したがって形式的証明は直観的ではなく、論理的誤りも少ない[1]。 1957年、多くの論理学者と計算機科学者が一堂に会した Cornell Summer が自動推論または自動定理証明の起源とされることがある[2]。それ以前のアレン・ニューウェル、クリフ・ショー、ハーバート・サイモンらが1955年に開発した Logic Theorist や、マーチン・デービスが1954年にプレスブルガーの決定手続きを実装したもの（2つの偶数の和が偶数であることを証明）[3]が起源だとすることもある。自動推論は重要な領域として盛んに研究が行われていたが、1980年代から90年代初頭の「AIの冬」の時代を経験し、その後運よく復興した。例えば2005年、マイクロソフトは多くの社内プロジェクトでのソフトウェア開発に検証技術を使い始め、Visual C++ の2012年版に論理的に検証する機能を追加した[2]。 アルフレッド・ノース・ホワイトヘッドとバートランド・ラッセルの『プリンキピア・マテマティカ』（数学原理）は数理論理学の画期をなした著作であり、あらゆる数式を論理によって導出することを目的として書かれた。同書は3巻に分かれており、それぞれ1910年、1912年、1913年に出版された[4]。 Logic Theorist (LT) は1956年、アレン・ニューウェル、クリフ・ショー、ハーバート・サイモンが開発した人間の行う推論を真似て定理を証明するプログラムであり、『プリンキピア・マテマティカ』の第2章にある52の定理のうち38を証明してみせた[5]。さらに言えば、単に証明しただけでなく、そのうちの1つはホワイトヘッドとラッセルが示した証明よりも洗練されていた。彼らは1958年にその成果を The Next Advance in Operation Research にて発表した。.mw-parser-output .templatequote{overflow:hidden;margin:1em 0;padding:0 40px}.mw-parser-output .templatequote .templatequotecite{line-height:1.5em;text-align:left;padding-left:1.6em;margin-top:0}今や世界には思考し、学習し、創造する機械が存在する。さらに、それらの能力は（近い将来）急速に適用範囲を広げようとしており、それと共に人の精神が扱える範囲も広がっていく。[6] 形式的証明の例年定理証明系形式化した人もともと証明した人 自動推論の最大の応用は自動定理証明機の構築である。時にはそういった証明機が定理の新たな証明方法をもたらすこともあり、Logic Theorist がよい例である。自動推論プログラムは、論理学、数学、計算機科学、論理プログラミング、ソフトウェアおよびハードウェアの設計検証、回路設計など様々な分野の問題を解くのに利用されている。TPTPはそういった問題を集めたライブラリであり、定期的に更新されている。また、CADE
歴史
重要な貢献
1986第1不完全性定理Boyer- MooreShankarゲーデル
1990平方剰余の相互法則Boyer- MooreRussinoffアイゼンシュタイン
1996微分積分学の基本定理HOL LightHarrisonHenstock
2000代数学の基本定理MizarMilewskiBrynski
2000代数学の基本定理CoqGeuvers 他クネーザー
2004四色定理CoqGonthierロバートソン他
2004素数定理IsabelleAvigad 他セルバーグ-エルデシュ
2005ジョルダン曲線定理HOL LightHalesThomassen
2005ブラウワーの不動点定理HOL LightHarrisonKuhn
2006Flyspeck 1IsabelleBauer- NipkowHales
2007コーシーの留数定理HOL LightHarrison古典的
2008素数定理HOL LightHarrison解析的証明
2012Feit?Thompsonの定理CoqGonthier 他Bender, Glauberman, Peterfalvi
主な証明システム
Boyer-Moore Theorem Prover (Nqthm)
LISPで構築された完全自動の定理証明機。ジョン・マッカーシーと Woody Bledsoe の影響を受けた設計である。1971年、スコットランドのエジンバラで開発が始まった。次のような特徴がある。
LISPにより論理を構築
すべてを再帰関数で定義することを基本としている。
「記号評価」と書き換えを多用。
記号評価の失敗に基づいた帰納的ヒューリスティックを使用[7]
HOL Light
OCamlで書かれており、論理的基盤が単純かつ明快になるよう設計され、実装もきれいである。古典的高階論理の証明を支援する[8]。
Coq
フランスで開発された証明支援システムで、仕様記述から実行可能なプログラムを自動生成できる（生成するソースコードはOCamlまたはHaskell）。仕様記述や証明の記述に使われる言語は Calculus of Inductive Constructions (CIC) と呼ばれている[9]。
応用
脚注^ Thomas, C. Hales. “ ⇒Formal Proof”. University of Pittsburgh. 2010年10月19日閲覧。
^ a b “ ⇒Automated Deduction (AD)”. The Nature of PRL Project. 2010年10月19日閲覧。
^ Martin Davis, "The Prehistory and Early History of Automated Deduction," in Automation of Reasoning, eds. Siekmann and Wrightson, vol. 1, 1-28 at p. 15
^ “ ⇒Principia Mathematica”. Stanford University. 2010年10月19日閲覧。
^ “ ⇒The Logic Theorist and its Children”. 2010年10月18日閲覧。
^ Shankar, Natarajan. “ ⇒Little Engines of Proof”. Computer Science Laboratory, SRI International. 2010年10月19日閲覧。
^ “ ⇒The Boyer- Moore Theorem Prover”. 2010年10月23日閲覧。
^ Harrison, John. “ ⇒HOL Light: an overview”. 2010年10月23日閲覧。