Loading article…
ジョン・アラン・ロビンソン | |
|---|---|
 2012年のロビンソン | |
| 生まれる | 1930年3月9日 イギリス、ウェスト・ヨークシャー州、ハリファックス |
| 死亡 | 2016年8月5日（享年86歳） 米国メイン州ポートランド |
| 母校 | ケンブリッジ大学 オレゴン大学 プリンストン大学 |
| 知られている | 解決原理、統一 |
| 受賞歴 | AMSマイルストーン賞 1985、フンボルト上級科学者賞 1995、エルブラン賞1996 |
| 科学者としてのキャリア | |
| 機関 | シラキュース大学 |
| 論文 | 因果関係、蓋然性、証言 （1957年） |
| 博士課程の指導教員 | カール・ヘンペル[1] |
ジョン・アラン・ロビンソン（1930年3月9日 - 2016年8月5日）は哲学者、数学者、コンピューター科学者であった。シラキュース大学の名誉教授であった。
アラン・ロビンソンの最大の貢献は、自動定理証明の基礎です。彼の統一アルゴリズムは、解決証明器における組み合わせ爆発の原因の 1 つを排除しました。また、特にProlog言語の論理プログラミングパラダイムの基礎も整えました。ロビンソンは、自動推論への顕著な貢献により1996 年にエルブラン賞を受賞しました。
人生
ロビンソンは1930年にイギリスのヨークシャー州ハリファックスで生まれ[2]、1952年にケンブリッジ大学で古典学の学位を取得して渡米した。オレゴン大学で哲学を学んだ後、プリンストン大学に移り、1956年に哲学の博士号を取得した。その後、デュポン社でオペレーションズリサーチアナリストとして働き、そこでコンピュータプログラミングを学び、独学で数学を学んだ。 1961年にライス大学に移り、夏はアルゴンヌ国立研究所の応用数学部門の客員研究員として過ごした。1967年にシラキュース大学の論理学およびコンピュータサイエンスの特別教授に就任し[3]、1993年に名誉教授となった。[4]
アルゴンヌでロビンソンは自動定理証明に興味を持ち、統一原理と解決原理を開発した。解決原理と統一原理はその後多くの自動定理証明システムに組み込まれ、論理プログラミングやプログラミング言語Prologで使用される推論メカニズムの基礎となっている。[5]
ロビンソン氏は『 Journal of Logic Programming』の創刊編集者であり、数々の栄誉を受けています。これらには、1967年のグッゲンハイムフェローシップ、1985年の自動定理証明におけるアメリカ数学会マイルストーン賞、 [6] 1990年のAAAIフェローシップ、[7] 1996年の自動推論への顕著な貢献に対するエルブランド賞、[8] [9] 1997年の論理プログラミング協会名誉称号「論理プログラミングの創始者」が含まれます。 [10]彼は、1988年にルーヴェンカトリック大学、[11] 1994年に ウプサラ大学、[12 ] 2003年にマドリード工科大学から名誉博士号を授与されています。 [13] [14]ロビンソンは、膵臓がんの手術後の破裂した動脈瘤のため、2016年8月5日にメイン州ポートランドで亡くなりました。[3]
1994年、ヴォルフガング・ビーベルの要請によりフンボルト上級科学者賞を受賞し、ダルムシュタット工科大学コンピュータサイエンス学部に6か月間滞在した。[15] [16]
主な出版物
- Robinson, J. Alan; Voronkov, Andrei編 (2001)。自動推論ハンドブック。MIT Press。ISBN 0-444-50813-9。
- Gabbay, Dov M .; Hogger, Christopher John; Robinson, JA, 編 (1993-1998)。人工知能と論理プログラミングにおけるロジックハンドブック。第 1 巻から第 5 巻、オックスフォード大学出版局。
- アービブ、マイケル A. ; ロビンソン、J .アラン編 (1990)。自然および人工並列計算。MITプレス。ISBN 0-262-01120-4。
- ロビンソン、JA（1979）。論理：形式と機能。エディンバラ大学出版局。ISBN 0-85224-305-7。
- Robinson, John Alan (1965 年 1 月)。「解決原理に基づくマシン指向ロジック」。J . ACM。12 ( 1 ): 23–41。doi : 10.1145/321250.321253。S2CID 14389185 。
- ロビンソン、ジョン・アラン (1957)。因果関係、蓋然性、証言(博士論文)。プリンストン大学。OCLC 83304635。
参照
- ロビンソンレゾルベント法ブール関数の最小化のためのクワイン・マクラスキー法の代替法
注記
- ^ “philosophyfamilytree record”. 2014年10月28日時点のオリジナルよりアーカイブ。2014年9月13日閲覧。
- ^ ジョン・アラン・ロビンソン CV、upm.es、アクセス日 2016 年 8 月 12 日
- ^ ab 「ジョン・アラン・ロビンソン、訃報」。ニューヨーク・タイムズ。2016年8月17日。 2019年11月2日閲覧。
- ^ シラキュース大学工学・コンピューターサイエンス名誉教授、2019年11月2日アクセス。
- ^ Coq開発チーム (2018年10月18日). Coqリファレンスマニュアル: リリース8.10+alpha (PDF) . p. 3. オリジナル(PDF)から2018年10月19日にアーカイブ。 2018年10月19日閲覧。
自動定理証明は、1960年代に命題論理学でデイビスとパトナムによって開拓されました。古典的な一階述語論理の完全な機械化 (半決定手続きの意味で) は、1965年にJAロビンソンによって、
解決
と呼ばれる単一の統一推論規則とともに提案されました。解決は、統一アルゴリズムを使用して、自由代数 (つまり項構造) 内の方程式を解くことに依存しています。解決の多くの改良は1970年代に研究されましたが、もちろんPROLOGがこの取り組みから生まれたことを除けば、納得のいく実装はほとんど実現されませんでした。
- ^ AMS 自動定理証明賞
- ^ AAAIフェローリスト
- ^ 「Herbrand Award 1996: J. Alan Robinson」。2007年3月7日時点のオリジナルよりアーカイブ。 2007年1月13日閲覧。
- ^ “CADE Herbrand Award”. 2014年9月13日時点のオリジナルよりアーカイブ。2014年9月13日閲覧。
- ^ ALP賞
- ^ KU Leuven 名誉博士号の概要 1966–2012
- ^ 「名誉博士号 - ウプサラ大学、スウェーデン」。2023年6月9日。
- ^ マドリード大学名誉博士号 1973–2013
- ^ ジョン・アラン・ロビンソンにマドリッド大学名誉博士号を授与、2003年10月1日
- ^ 「フンボルトネットワークにおけるジョン・アラン・ロビンソンのプロフィール」www.humboldt-foundation.de 。 2019年11月2日閲覧。[永久リンク切れ]
- ^ Leonhard Wolfgang Bibel (2017)、Reflexionen vor Reflexen - Memoiren eines Forschers (ドイツ語) (1 版)、ゲッティンゲン: Cuvillier Verlag、ISBN 9783736995246