氏名

高橋 優太 (TAKAHASHI Yuta)

所属

ソフトウェア情報学部ソフトウェア情報学科

職種講師

生年月日
[履歴]

[学歴]

1985 年 2 月 21 日

2014 年 3 月慶應義塾大学文学研究科哲学・倫理学専攻後期博士課程所定単位取得退学
2009 年 3 月慶應義塾大学文学研究科哲学・倫理学専攻前期博士課程修了
2007 年 3 月茨城大学人文学部人文学科哲学専攻卒業[学位]

博士(哲学)(2017 年 10 月 慶應義塾大学)[職歴]2024 年 4 月～ 青森大学ソフトウェア情報学部ソフトウェア情報学科 講師
2024 年 4 月～ 慶應義塾大学未来共生デザイン研究センター 共同研究員
2022 年 4 月～ 早稲田大学文化構想学部 非常勤講師
2021 年 10 月～ 慶應義塾大学文学部 非常勤講師
2021 年 10 月～2024 年 3 月 お茶の水女子大学文理融合 AI・データサイエンスセンター 特任助教
2015 年 4 月～2024 年 3 月 慶應義塾大学論理と感性のグローバル研究センター 共同研究員
2021 年 7 月～2021 年 9 月 名古屋大学大学院情報学研究科 研究員
2019 年 7 月～2021 年 7 月 パリ第 1 パンテオン・ソルボンヌ大学 IHPST 訪問研究員(日本学術振興会・海外特別研究員)
2016 年 4 月～2019 年 9 月 慶應義塾大学理工学部 非常勤講師
2014 年 4 月～2019 年 9 月 慶應義塾大学文学部 非常勤講師
2017 年 4 月～2019 年 3 月 芝浦工業大学デザイン工学部 非常勤講師
2016 年 4 月～2019 年 3 月 名古屋大学大学院情報学研究科 日本学術振興会・特別研究員 PD2015 年 4 月～2016 年 3 月 慶應義塾大学文学研究科 非常勤助教(有期・研究奨励)2013 年 10 月～2014 年 3 月 慶應義塾大学論理と感性の先端的教育研究拠点形成 RA
研究員
2012 年 4 月～2014 年 3 月 慶應義塾大学文学研究科 非常勤助教(有期・研究奨励)[受賞]2014 年 11 月 2013 年度科学基礎論学会奨励賞「ゲンツェンを読む―三つの無矛盾性証
明の統一的解釈―」秋吉 亮太、高橋 優太[所属学会]

応用哲学会
科学基礎論学会
言語処理学会
人工知能学会
日本論理哲学会
日本科学哲学会[教育活動][担当科目]

プログラミング演習Ⅰ・Ⅱ、キャリアデザイン B[卒業研究指導]なし[ゼミ指導]

ソフトウェア情報学基礎ゼミナール A・B[教育指導に関する特記事項]

なし[研究活動][研究テーマ]

数学基礎論、情報科学における論理学[論文]

1. Natsuki Murakami, Mana Ishida, Yuta Takahashi, Hitomi Yanaka, Daisuke Bekki.
Knowledge Injection for Disease Names in Logical Inference between Japanese
Clinical Texts. Proceedings of the 5th Clinical Natural Language Processing

Workshop. 108-117, 2023.
2. 小斉平 ひな, 高橋 優太, 戸次 大介.「依存型意味論の未指定型による照応解析の試み」．2023 年度人工知能学会全国大会論文集（第 37 回）．2023.
3. 村上 夏輝, 石田 真捺, 高橋 優太, 谷中 瞳, 戸次 大介.「病名知識の公理補完を用いた症例テキスト間の論理推論」．2023 年度人工知能学会全国大会論文集（第 37回）
．2023.
4. 飯沼 瑞稀, 高橋 優太, 田上 青空, 戸次 大介.「型検査アルゴリズムを用いた
Neural DTS のための推論手続きの試み」．2023 年度人工知能学会全国大会論文集（第37 回）．2023.
5. Daisuke Bekki, Ribeka Tanaka, Yuta Takahashi. Integrating Deep Neural Networks
with Dependent Type Semantics. Logic and Algorithms in Computational

Linguistics 2021 (LACompLing2021). 261-284. 2023.
6. 小斉平 ひな, 高橋 優太, 戸次 大介.「証明支援系 Coq を用いた依存型意味論の照応解析と推論の実装の試み」．言語処理学会 第 29 回年次大会 発表論文集．
2978-2983. 2023.
7. 飯沼 瑞稀, 高橋 優太, 田上 青空, 戸次 大介. 「Neural DTS に対する型検査アルゴリズムの実装の試み」．言語処理学会 第 29 回年次大会 発表論文集．2161-2165.
2023.
8. Daisuke Bekki, Ribeka Tanaka, Yuta Takahashi. Learning Knowledge with NeuralDTS. Proceedings of the 3rd Natural Logic Meets Machine Learning Workshop(NALOMA III). 17-25. 2022.
9. Yuta Takahashi. Size-Based Termination for Non-Positive Types in Simply Typed
Lambda-Calculus. 27th International Conference on Types for Proofs andPrograms (TYPES 2021). Leibniz International Proceedings in Informatics(LIPIcs) 239. 2022.
10. Alberto Naibo, Yuta Takahashi. Harmony in the Light of Computational Ludics.

Electronic Proceedings in Theoretical Computer Science 353 132-156. 2021.
11. Mitsuhiro Okada, Yuta Takahashi. A Simplified Application of Howard’s Vector
Notation System to Termination Proofs for Typed Lambda-Calculus Systems.

Rewriting Logic and Its Applications (WRLA 2020). 136-155. 2020.
12. Yuta Takahashi, Ryo Takemura. Completeness of Second-Order Intuitionistic
Propositional Logic with Respect to Phase Semantics for Proof-Terms. Journalof Philosophical Logic 48 553-570. 2019.
13. Mitsuhiro Okada, Yuta Takahashi. On Quasi Ordinal Diagram Systems. Proceedings

Tenth International Workshop on Computing with Terms and Graphs (TERMGRAPH
2018), Oxford, UK, 7th July 2018. Electronic Proceedings in TheoreticalComputer Science 288 38-49. 2019.
14. Yuta Takahashi. On the Intuitionistic Background of Gentzen's 1935 and 1936
Consistency Proofs and Their Philosophical Aspects. Annals of the Japan
Association for Philosophy of Science 27 1-26. 2018.
15. Ryota Akiyoshi, Yuta Takahashi. Contentual and Formal Aspects of Gentzen'sConsistency Proofs. Philosophical Logic: Current Trends in Asia 95-137. 2017.
16. 高橋 優太.「1 階算術に対するゲンツェンの 1935 年版無矛盾性証明がもつ哲学的意義―含意を巡る循環との関わりにおいて―」．科学哲学 49(1) 49-66. 2016.

17. 高橋 優太.「ゲンツェンの 1935 年版無矛盾性証明と含意解釈」．哲學 (三田哲学会編) 135 45-58. 2015.
18. Yuta Takahashi. Gentzen's First Consistency Proof of Arithmetic, andIntuitionistic Mathematics. 平成 25 年度論理と感性の先端的教育研究拠点形成プ
ログラム研究報告 19-32. 2014.
19. 秋吉 亮太, 高橋 優太.「ゲンツェンを読む―三つの無矛盾性証明の統一的解釈―」．
科学基礎論研究 41(1) 1-22. 2013.
20. 高橋 優太.「フレーゲにおける論理的分析の方法と分析のパラドクス」．哲学の探求37 98-120. 2010.
[学会発表]

1. Yuta Takahashi. Type Checking for Logical Approach to Natural Language
Inference. French-Japanese Colloquium: Disagreement in logic and reasoning.
2024 年 3 月 26 日.
2. Hina Kosaihira, Yuta Takahashi, Daisuke Bekki. Implementation of Anaphora
Resolution Using the Refine Tactic of Coq. 2023 Workshop on Proof Theory andits Applications. 2023 年 7 月 14 日.
3. Yuta Takahashi. Towards an Interpretation of Inaccessible Sets in Martin-Löf
Type Theory with One Mahlo Universe. TYPES 2023: 29th International Conference
on Types for Proofs and Programs. 2023 年 6 月 13 日.
4. 小斉平 ひな, 高橋 優太, 戸次 大介. 依存型意味論の未指定型による照応解析の試み．2023 年度 人工知能学会全国大会（第 37 回）．2023 年 6 月 7 日.
5. 村上 夏輝, 石田 真捺, 高橋 優太, 谷中 瞳, 戸次 大介. 病名知識の公理補完を用いた症例テキスト間の論理推論．2023 年度 人工知能学会全国大会（第 37 回）．
2023 年 6 月 7 日.
6. 飯沼 瑞稀, 高橋 優太, 田上 青空, 戸次 大介. 型検査アルゴリズムを用いた
Neural DTS のための推論手続きの試み．2023 年度 人工知能学会全国大会（第 37回）
．2023 年 6 月 7 日.
7. 小斉平 ひな, 高橋 優太, 戸次 大介. 証明支援系 Coq を用いた依存型意味論の照応解析と推論の実装の試み．言語処理学会第 29 回年次大会(NLP2023). 2023 年 3 月16 日.
8. 飯沼 瑞稀, 高橋 優太, 田上 青空, 戸次 大介. Neural DTS に対する型検査アルゴ
リズムの実装の試み．言語処理学会第 29 回年次大会(NLP2023). 2023 年 3 月 15 日.
9. Yuta Takahashi. Higher-Order Universe Operators in Martin-Löf Type Theory withone Mahlo Universe. TYPES 2022: 28th International Conference on Types forProofs and Programs 2022 年 6 月 23 日.
10. 高橋 優太. 論理推論とは何か―証明論的意味論の観点から―．慶應義塾大学論理と感性のグローバル研究センター2021 年度末成果報告会．2022 年 3 月 3 日.
11. Yuta Takahashi. On Gentzen's Consistency Proofs: A Case of Disagreement between
Intuitionism and Formalism. Aspects of Logic Study. 2022 年 1 月 15 日.
12. Daisuke Bekki, Ribeka Tanaka, Yuta Takahashi. Integrating Deep Neural Networkwith Dependent Type Semantics. Logic and Algorithms in Computational
Linguistics 2021 (LACompLing2021). 2021 年 12 月 16 日.
13. 高橋 優太. マーティン-レーフ型理論における対象の同一性基準について．日本論
理哲学会第 25 回大会．2021 年 12 月 4 日.
14. Alberto Naibo, Yuta Takahashi. Fixed-point operators: from proof-theoretic
semantics

tocomputation.

EXPRESS-IHPST

workshop:

Truth,proofandcommunication. 2021 年 6 月 22 日.
15. Yuta Takahashi. Size-Based Termination for Non-Positive Types. TYPES 2021:
27th International Conference on Types for Proofs and Programs. 2021 年 6 月14 日.
16. Mitsuhiro Okada, Yuta Takahashi. A Simplified Application of Howard's Vector
Notation System to Termination Proofs for Typed Lambda-Calculus Systems. The
13th International Workshop on Rewriting Logic and its Applications (WRLA 2020)
online event. 2020 年 10 月 22 日.
17. Alberto Naibo, Yuta Takahashi. Harmony in the Light of Computational Ludics.
2020 Joint Workshop Linearity & Trends in Linear Logic and its Applications.
2020 年 6 月 30 日.
18. Yuta Takahashi. Gentzen's consistency proofs and the implication ofintuitionistic logic: A viewpoint of Okada. Mathematical and logicalunderstanding and formalization: Workshop in honor of Pr. Mitsuhiro Okada. 2020年 2 月 10 日.
19. Yuta Takahashi. On a disagreement about the finiteness of Gentzen's 1935
consistency proof for first-order arithmetic. Workshop "Norm, Rule andDisagreement". 2019 年 1 月 11 日.
20. 高橋 優太. 証明図の集合から意味論をつくる．日本論理哲学会第 22 回大会 アルカ
ディア市ヶ谷(私学会館). 2018 年 12 月 1 日.
21. Yuta Takahashi. Phase Semantic Investigation into Proof-terms of Second-order
Intuitionistic Propositional Logic. 2nd Nagoya Meta-Philosophy Workshop. 2018年 11 月 5 日.
22. Mitsuhiro Okada, Yuta Takahashi. On quasi ordinal diagram systems. TERMGRAPH
2018. 2018 年 7 月 7 日.
23. Mitsuhiro Okada, Yuta Takahashi. Ordinal Diagrams and Well-Quasi-Orderings

(preliminary report). French-Japanese Workshop "Philosophy of Logic andMathematics" with special focuses on "Philosophy of Proofs" and the Study ofEuclid's Elements. 2018 年 1 月 20 日.
24. 高橋 優太. 数学的推論と論理的推論との区別に関するデトレフセン・ポアンカレ説について．日本論理哲学会第 21 回大会 アルカディア市ヶ谷(私学会館). 2017 年 12月 2 日.
25. 高橋 優太. ゲンツェンによる算術の無矛盾性証明とヒルベルト・ブラウワー論争．
数理哲学史夏期合宿セミナー 草津セミナーハウス．2017 年 9 月 23 日.
26. Yuta Takahashi. A Proof-theoretic Semantics for Disjunction. Logic Colloquium
2017. 2017 年 8 月 17 日.
27. Yuta Takahashi. Phase Semantics as Proof-Theoretic Semantics. French-JapaneseWorkshop "Philosophy of logic and Mathematics -- Towards Philosophy of Proofs".
2017 年 1 月 13 日.
28. Yuta Takahashi, Ryo Takemura. On Completeness of Second-Order Intuitionistic
Propositional Logic and Proof-Theoretic Semantics a la Prawitz. Workshop on
philosophy of logic: Logic, computation and normativity. 2016 年 11 月 11 日.
29. Yuta Takahashi, Ryo Takemura. Completeness of Second-Order Intuitionistic
Propositional Logic with Respect to a Proof-Theoretic Semantics. The joint
Conference of The 3rd Asian Workshop on Philosophical Logic (AWPL-2016) & The
3rd Taiwan Philosophical Logic Colloquium (TPLC-2016). 2016 年 10 月 8 日.
30. Ryota Akiyoshi, Yuta Takahashi. Contentual and Formal Aspect of Gentzen'sConsistency Proofs. The joint Conference of The 3rd Asian Workshop on
Philosophical Logic (AWPL-2016) & The 3rd Taiwan Philosophical LogicColloquium (TPLC-2016). 2016 年 10 月 5 日.
31. 高橋 優太. ゲンツェンによる算術の無矛盾性証明について―1935 年論文に基づいた含意解釈．論理と感性のグローバル研究センター 論理班 年度末報告会．2016 年
1 月 29 日.
32. YutaTakahashi.

NormalizationinGentzen's

1935

Consistency

Proof.

French-Japanese Workshop on Philosophy of Proofs. 2016 年 1 月 15 日.
33. 高橋 優太. ゲンツェンの無矛盾性証明と「含意を巡る循環」．日本論理哲学会第 19回大会 アルカディア市ヶ谷(私学会館). 2015 年 12 月 5 日.
34. 高橋 優太. ゲンツェンにより指摘された「含意を巡る循環」について．日本科学哲学会第 48 回(2015 年)大会．2015 年 11 月 22 日.
35. Yuta Takahashi. Gentzen's 1935/36 Consistency Proofs as Means of Ascribing
Constructive Senses. "Philosophy of Mathematics and Proof Theory" Workshop.
2015 年 9 月 11 日.

36. Yuta Takahashi. Gentzen's 'Finitist' Interpretation in the Context of theFormalism-Intuitionism Controversy. 15th Congress on Logic, Methodology, andPhilosophy of Science. 2015 年 8 月 8 日.
37. Ryota Akiyoshi, Yuta Takahashi. A Uniform Idea behind Gentzen's Three
Consistency Proofs. Logic Colloquium 2015. 2015 年 8 月 4 日.
38. Yuta Takahashi. The Intuitionistic Background of Gentzen's 1935/36 Consistency
Proofs. Workshop on Philosophy of Logic. 2015 年 2 月 27 日.
39. Yuta Takahashi. The Intuitionistic Background of Gentzen's Finitist
Interpretation. The 2nd Conference on Contemporary Philosophy in East Asia.
2014 年 8 月 28 日.
40. Yuta Takahashi. On the Finitist Interpretation of Implications by Gentzen's
1935 Consistency Proof. Functions, Proofs, Constructions. 2014 年 2 月 21 日.
41. 高橋 優太. The Analysis of Logical Implication from Gentzen's Finitary Pointof View. 平成 25 年度 文部科学省 卓越した大学院拠点形成支援補助金 「論理と感性の先端的教育研究拠点形成」 RA 研究員年度末報告会．2014 年 2 月 3 日.
42. Yuta Takahashi. Gentzen's 1935 Consistency Proof and the Interpretation ofImplication. 23rd World Congress of Philosophy. 2013 年 8 月 6 日.
43. Yuta Takahashi. On Philosophical Significance of Gentzen's Finitism. CAPE
International Workshop of Constructivism. 2013 年 3 月 1 日.
44. 高橋 優太. ゲンツェンの有限主義とバー定理．日本科学哲学会第 45 回（2012 年）大会．2012 年 11 月 10 日.
45. 高橋 優太. ゲンツェンの証明が与える概念分析．科学基礎論学会 2012 年度総会と講演会．2012 年 6 月 17 日.
46. Yuta Takahashi. Another Aspect of Gentzen's Program. 1st Seoul Philosophy
Graduate Student Conference. 2012 年 5 月 6 日.
47. 高橋 優太. ゲンツェンと自然数論の命題の意味．日本科学哲学会第 44 回（2011年）大会．2011 年 11 月 19 日.
48. 高橋 優太. フレーゲとヒルベルト的形式主義．慶應義塾大学グローバル COE プロ
グラム論理と感性の先端的教育研究拠点：数学の哲学セミナー．2011 年 9 月 16 日.
49. Yuta Takahashi. Frege's Proof of Consistency and Extensions of Concepts. Global
COE Symposium "Toward an Integration of Logic and Sensibility -- fromNeuroscience to Philosophy --". Poster presentation. 2011 年 9 月 14 日.
50. 高橋 優太. 『基本法則』における概念の外延．科学基礎論学会 2011 年度総会と講演会．2011 年 6 月 5 日.
51. 高橋 優太. 論理法則の正当化に対するフレーゲのアプローチ．日本科学哲学会第43 回(2010 年)大会．2010 年 11 月 27 日.

52. 高橋 優太. フレーゲにおける論理的分析の方法と分析のパラドクス．2009 年度哲
学若手研究者フォーラム．2009 年 7 月 19 日.
[その他の活動]なし[公開講座、講演、セミナー]

1. 高橋優太. ヒルベルトのε計算（チュートリアル）．数学基礎論サマースクール
2018：証明論，特に算術の無矛盾性証明．2018 年 9 月 5 日.
[学内各種委員]
付属総合研究所運営委員会、図書委員会