クリストフ・ベンツミュラー
クリストフ・エーヴァルト・ベンツミュラー | |
|---|---|
 バンベルクのクリストフ・ベンツミュラー (2025) | |
| 生まれる | 1968年（57～58歳） |
| 母校 | ザールラント大学 |
| 知られている | 形式的推論定理証明 |
| 科学者としてのキャリア | |
| 機関 | バンベルク大学ベルリン自由大学 |
| 論文 | 高階定理証明における等式と拡張性[ 1 ] (1999) |
| 博士課程の指導教員 | ヨルグ・H・シークマンマイケル・コールハーゼフランク・フェニング |
クリストフ・エーヴァルト・ベンツミュラー（1968年生まれ）[ 2 ]はドイツのコンピュータ科学者であり、記号的人工知能を用いた合理的議論の形式化を研究対象としている。 2022年からバンベルク大学でAIシステム工学の教授を務め、2021年からはベルリン自由大学で教授を務めている。[ 3 ]
教育とキャリア
ベンツミュラーは1989年からザールラント大学でコンピュータサイエンスを学び、1995年に学位を取得。その後、 1999年にイェルク・H・ジークマンの指導の下、「高階定理証明における等式と外延性」というテーマで博士号を取得。指導教員はミヒャエル・コールハーゼとフランク・フェニング。[ 1 ] バーミンガムとエディンバラで留学した後、 2001年から2008年までザールラント大学で講師を務め、ケンブリッジでも研究を行った。その後、2009年までドイツのブルッフザール国際大学で教授を務めた。ベンツミュラーは2008年にザールラント大学で、2012年にベルリン自由大学で博士号を取得した。 2021年からベルリン自由大学の教授を務めている。2022年2月にはバンベルク大学の教授に就任した。[ 4 ]
認識
ベンツミュラーは、人工知能、哲学、数学、言語処理の交差点で研究を行っています。一方では、哲学/形而上学と数学への応用を伴う形式推論と普遍論理に興味を持ち、他方では、AIシステムの倫理的および法的制御のためのハイブリッドAI技術の開発に興味を持っています。研究滞在や客員教授職の枠内で、ルクセンブルク大学、スタンフォード大学（米国）、ケンブリッジ大学（英国）、カーネギーメロン大学（米国）、ドバイBITSピラニ（UAE）、浙江大学（中国）など、数多くの国際機関と協力関係を築いてきました。さまざまな国際委員会で委員を務め、AIスタートアップ企業に助言を行い、欧州人工知能研究研究所連合（CLAIRE-AI）の国内連絡担当者、ベルリン数学研究センター大学院（MATH+）およびドイツ科学者連盟のメンバーでもあります。[ 4 ]
彼は、2014年と2025年のゲーデルの存在論的証明の形式化の研究[ 5 ] [ 6 ]と、 2016年のIsabelleによる自動定理証明を用いた定理の検証[7]で最もよく知られています。[ 8 ] [ 9 ] [ 10 ]証明は、ウィーン工科大学の研究者によって確認されました。[ 6 ] [ 11 ]形式化と証明により、ベンツミュラーは国内の報道機関[ 12 ] [ 13 ] [ 14 ] や国際的に学際的な研究者から注目を集めました。[ 15 ]
私生活
私生活では、ベンツミュラーは競技アスリートとして活躍しており[ 2 ]、若い頃には長距離走者とハードル走者として数々の優勝を果たした。結婚しており、3人の子供がいる[ 16 ] 。
参考文献
- ^ a b高階定理証明における等式と拡張性、ザールラント大学図書館、2022年6月29日、2024年10月15日閲覧。
- ^ a b "Christoph Benzmüller Leistungsentwicklung" (ドイツ語)。
- ^ FU Berlin 、 2024年12月25日閲覧。
- ^ a b CV (PDF) 、 2024年10月15日閲覧
- ^ Christoph BenzmüllerとBruno Woltzenlogel-Paleo (2014). 「高階自動定理証明器によるゲーデルの神の存在論的証明の自動化」(PDF) .欧州人工知能会議議事録. 人工知能とその応用の最前線. 第263巻. IOS Press. pp. 93– 98. 2014年7月14日時点のオリジナルよりアーカイブ(PDF) 。
- ^ a b "形式神学/ゲーデル神" . GitHub。 2021年6月28日。
- ^ Christoph BenzmüllerとDana Scott . 「ゲーデルとスコットの存在論的論証の変種に関する注釈」 Monatsh Math . doi : 10.1007/s00605-025-02078-x .
- ^ Christoph BenzmüllerとBruno Woltzenlogel-Paleo (2016年7月). 「ゲーデルの存在論的論証における矛盾：形而上学におけるAIの成功物語」(PDF) . Subbarao Kambhampati (編). Proc. 25th International Joint Conference on Artificial Intelligence . AAAI Press. pp. 936– 942. 2016年11月13日時点のオリジナルよりアーカイブ(PDF) .
- ^ Christoph BenzmüllerとDavid Fuenmayor (2017年5月). 「Isabelle/HOLにおける型、タブロー、そしてゲーデルの神」 . Archive of Formal Proofs . ISSN 2150-914X .
- ^ Isabelle/HOL の Types, Tableaus and Gödel's God 、 2024年12月25日閲覧
- ^ベルリン大学出版局、2013年10月17日、 2024年12月25日閲覧
- ^ G(x) = Gott (ドイツ語) 、 2024年12月25日閲覧
- ^ FU-Lehrpreis für Christoph Benzmüller: Der Gottesbeweiser (ドイツ語) 、 2024 年 12 月 25 日取得
- ^ KI-Forscher: Reale Existenz Gottes nicht absolut sicher, aber... (ドイツ語) 、 2024 年 12 月 25 日取得
- ^計算形而上学の実験：ゲーデルによる神の存在の証明（ドイツ語） 、 2024年12月25日閲覧
- ^ 「Die schnellste deutsche 13-Jährige läuft für Trier – und trainiert in Dubai」（ドイツ語）。
外部リンク
