重要な貢献
出典: フリー百科事典『ウィキペディア（Wikipedia）』 (2019/11/13 06:25 UTC 版)
アルフレッド・ノース・ホワイトヘッドとバートランド・ラッセルの『プリンキピア・マテマティカ』（数学原理）は数理論理学の画期をなした著作であり、あらゆる数式を論理によって導出することを目的として書かれた。同書は3巻に分かれており、それぞれ1910年、1912年、1913年に出版された。 Logic Theorist (LT) は1956年、アレン・ニューウェル、クリフ・ショー、ハーバート・サイモンが開発した人間の行う推論を真似て定理を証明するプログラムであり、『プリンキピア・マテマティカ』の第2章にある52の定理のうち38を証明してみせた。さらに言えば、単に証明しただけでなく、そのうちの1つはホワイトヘッドとラッセルが示した証明よりも洗練されていた。彼らは1958年にその成果を The Next Advance in Operation Research にて発表した。 今や世界には思考し、学習し、創造する機械が存在する。さらに、それらの能力は（近い将来）急速に適用範囲を広げようとしており、それと共に人の精神が扱える範囲も広がっていく。 形式的証明の例年定理証明系形式化した人もともと証明した人1986 第1不完全性定理 Boyer- Moore Shankar ゲーデル 1990 平方剰余の相互法則 Boyer- Moore Russinoff アイゼンシュタイン 1996 微分積分学の基本定理 HOL Light Harrison Henstock 2000 代数学の基本定理 Mizar Milewski Brynski 2000 代数学の基本定理 Coq Geuvers 他 クネーザー 2004 四色定理 Coq Gonthier ロバートソン他 2004 素数定理 Isabelle Avigad 他 セルバーグ-エルデシュ 2005 ジョルダン曲線定理 HOL Light Hales Thomassen 2005 ブラウワーの不動点定理 HOL Light Harrison Kuhn 2006 Flyspeck 1 Isabelle Bauer- Nipkow Hales 2007 コーシーの留数定理 HOL Light Harrison 古典的 2008 素数定理 HOL Light Harrison 解析的証明 2012 Feit–Thompsonの定理 Coq Gonthier 他 Bender, Glauberman, Peterfalvi
※この「重要な貢献」の解説は、「自動推論」の解説の一部です。
「重要な貢献」を含む「自動推論」の記事については、「自動推論」の概要を参照ください。
- 重要な貢献のページへのリンク
