岡田 光弘 (オカダ ミツヒロ)

Okada, Mitsuhiro

写真a

所属(所属キャンパス)

文学部 哲学専攻 (三田)

職名

名誉教授

HP

外部リンク

プロフィール 【 表示 / 非表示

  • 論理的思考の解明に向けて――論理推論の学際的統合研究  論理学という学問は紀元前4世紀にアリストテレスにより定式化されて以来現在まで研究が蓄積されてきた、最も古い学問分野の一つです。また、論理学の文脈の中で1936年に現代のコンピュータ理論が誕生しました。しかし論理学や論理思考の研究分野には21世紀の現在も、まだ解明されていない問題が数多くあります。私は論理や論理推論の研究を通じて人間の思考の解明を目指しています。平成25年度もこの目的で、哲学を中心に、数理論理学的観点、計算機科学・情報科学的観点、認知科学的観点、神経科学的観点などを含む学際的観点から、論理学を多面的に研究してきました。  平成25年度の研究には以下のものがあります。 1.哲学的論理  20世紀を代表するウィトゲンシュタイン、フッサールなどの哲学者たちの論証と計算の理論、数学の哲学について現代的に再評価する観点を提示しました。 2.認知科学手法  情報科学的手法などp取り入れてと論理的判断の研究を進めています。ライプニッツ、オイラーなどから始まる図形的論理推論、グラフィック推論の理論を理論と被験者調査研究の両面から研究しています。 3.論理構造の理論研究  線形論理と呼ばれる基底的な論理構造(古典論理と直感的論理の区別以前の論理)に対して、それをさらに分解してより基底的な論理推論群から線形論理を構成する基礎理論研究を進めました。 4.情報ネットワーク社会が直面する諸問題を論理学的観点から考察しています。セキュリティプロトコルの論理的安全性証明、セキュリティとプライバシーの問題、アルゴリズムの公平性、等の問題が挙げられます。2013年開設以来私が所長を務める「論理と感性のグローバル研究センター」(先導研傘下)の学際的研究環境の下でも進めています。

その他の所属・職名 【 表示 / 非表示

  • 論理と感性のグローバル研究センター, センター共同研究員

  • 玉川大学脳科学研究所, 脳科学研究所, 共同研究員(客員教授)

  • パリ第1大学, 科学・技術史科学・技術哲学研究所(IHPST), Associate Member (連携研究員)

経歴 【 表示 / 非表示

  • 1998年04月
    -
    2020年03月

    慶應義塾大学, 大学院文学研究科, 委員

  • 1996年04月
    -
    2020年03月

    慶應義塾大学, 文学部, 教授

  • 1990年09月
    -
    1996年03月

    慶應義塾大学, 文学部, 助教授

  • 2017年03月
    -
    継続中

    パリ第1大学 科学史哲学研究所(IHPST), 科学史哲学研究所(IHPST), 学外連携所員

  • 2001年02月

    パリ第1大学(パンテオン=ソルボンヌ), 哲学科, 招聘教授

全件表示 >>

学歴 【 表示 / 非表示

  • 1979年03月

    東京大学, 文学部, 哲学科

    大学, 卒業

  • 1983年03月

    慶應義塾, 文学研究科

    大学院, 修了, 修士

  • 1987年03月

    慶應義塾, 文学研究科

    大学院, 修了, 博士

学位 【 表示 / 非表示

  • 文学博士 , 慶應義塾, 課程, 1987年03月

    弱い含意に制限した論理について

 

研究分野 【 表示 / 非表示

  • 哲学・倫理学 (哲学・倫理学 / 論理の哲学、数学の哲学、ウィトゲンシュタイン研究、情報論理、フッサール論理学、アルゴリズムの倫理、意思決定と推論の心理学)

研究キーワード 【 表示 / 非表示

  • Computer security

  • Diagrammatic logic

  • Theoretical computer science

  • AIの哲学

  • アルゴリズムの倫理

全件表示 >>

共同研究希望テーマ 【 表示 / 非表示

  • 論理的思考、推論能力、意思決定、情報論理及び情報倫理, 図的・グラフィック推論と意思決定、 思考の学際科学、論理と認知科学

    大学等の研究機関との共同研究を希望する

     メッセージを見る

    特に次のテーマに関して応用面に興味を持っている。1.論理推論の教育デザイン、論理推論略評価法、評価課題集などを開発してきた。
    2.図的・グラフィック情報提示に基づく意思決定・論理推論の研究地球蓄積を持ち、社会心理学的消費者行動意思決定への応用研究に関わる研究を進めている。

 

著書 【 表示 / 非表示

  • Wittgenstein and Goodstein on Uniqueness of Primitive recursive arithmetic, in "Wittgenstein in the 1930s:Investigations to Philosophical Investigations" (ed. by David Stern)

    Mathieu Marion and Mitsuhiro Okada, Cambridge University Press, 2018年11月

    担当範囲: Chapter authors

  • A Report of Reserch Center for Thinkingand and Behavioral Judgement

    Mitsuhiro Okada, Research Centre for Thinking and Behavioral Judgment, Keio University, 2014年12月

  • Effects of Representation Patterns in Multi-Attribute Decision-Making: An Eye-Tracking Study

    Mitsuhiro Okada, Research Centre for Thinking and Behavioral Judgment, Keio University, 2014年12月

  • Eye-Tracking Study of Decision-Making with Graphically Represented Multi-Attribute Tables.

    Okubo,S.& Okada,M., Report of the Reserch Center for Thinking and Behavioral Judgement(ed.M.Okada et al.),Keio University, 2014年

    担当範囲: 17-23

  • La philosophiedes mathmatiques de Wittgenstein Wittgenstein(eds.Christine Chauvire and Sabine Plaud)

    Mathieu Marion and Mitsuhiro Okada, Ellipes, 2012年

    担当範囲: 79-103

全件表示 >>

論文 【 表示 / 非表示

  • On Effects of Changing Multi-attribute Table Design on Decision Making: An Eye-Tracking Study

    Ideno T., Morii M., Takemura K., Okada M.

    Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics))  12169 LNAI   365 - 381 2020年

    ISSN  9783030542481

     概要を見る

    Information tables are often used for decision making. This study considers multi-attribute table designs from a diagrammatic perspective. We used two experiments to show how the decision-making strategies and performance are changed based on table design changes, using the eye-tracking method. We employed a multi-attribute catalog table with alternatives presented along the horizontal axis and attributes along the vertical axis in Experiment 1 and the opposite layout in Experiment 2. In each experiment, we used four different types of representations of the attribute values, and these values were restricted to two levels for comparison with previous works. The four types used were: (i) numerical representations, (ii) textual representations, (iii) black-and-white representations with black representing better values, and (iv) black-and-while representations with white representing better values. Our results suggest, among others, that (1) placing the alternatives along the vertical axis makes the table easier to decide in comparison to the opposite layout, and that (2) the two-stage decision strategy is taken with numerical representations and textual representations, while a single stage strategy is taken with the black-and-white representations. We also showed how the graphic black-and-white representations made decision-making easier, and how the order changes of alternatives and of attributes of a table influenced decision makers’ decision.

  • A Small Remark on Hilbert’s Finitist View of Divisibility and Kanovich-Okada-Scedrov’s Logical Analysis of Real-Time Systems

    Okada M.

    Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics))  12300 LNCS   39 - 47 2020年

    ISSN  03029743

     概要を見る

    Hilbert remarked in the introductory part of his most famous finitism address (1925 [1]) that “[t]he infinite divisibility of a continuum is an operation that is present only in our thought”, which means that no natural event or matter is infinitely divisible in reality. We recall that Scedrov’s group including the author started logical analysis of real time systems with the principle similar to Hilbert’s no-infinite divisibility claim, in [2]. The author would like to note some early history of the group’s work on logical analysis of real time system as well as some remark related to Hilbert’s claim of no-infinite divisibility.

  • A Simplified Application of Howard’s Vector Notation System to Termination Proofs for Typed Lambda-Calculus Systems

    Okada M., Takahashi Y.

    Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics))  12328 LNCS   136 - 155 2020年

    ISSN  9783030635947

     概要を見る

    There have been some important methods of combining a recursive path ordering and Tait-Girard’s computability argument to provide an ordering for termination proofs of higher-order rewrite systems. The higher-order recursive path ordering HORPO by Jouannaud and Rubio and the computability path ordering CPO by Blanqui, Jouannaud and Rubio are examples of such an ordering. In this paper, we give a case study of yet another direction of such extension of recursive path ordering, avoiding Tait-Girard’s computability method plugged in the above mentioned works. This motivation comes from Lévy’s question in the RTA open problem 19, which asks for a reasonably straightforward interpretation of simply typed λ -calculus λ in a certain well founded ordering. As in the cases of HORPO and CPO, the addition of λ -abstraction and application into path orderings might be considered as one solution, but the following question still remains; can the termination of λ be proved by an interpretation in a first-order well founded ordering in the sense that λ -abstraction/application are not directly built in the ordering? Reconsidering one of Howard’s works on proof-theoretic studies, we introduce the path ordering with Howard algebra as a case study towards further studies on Lévy’s question. → →

  • Verification Methods for the Computationally Complete Symbolic Attacker Based on Indistinguishability

    GERGEI BANA, ROHIT CHADHA, AJAY KUMAR EERALLA, MITSUHIRO OKADA

    ACM Trans. Comput. Logic (Association for Computing Machinery)  to appear ( 1 )  2019年12月

    研究論文(学術雑誌), 査読有り,  ISSN  15293785

     概要を見る

    © 2019 Copyright held by the owner/author(s). In recent years, a new approach has been developed for verifying security protocols with the aim of combining the benefits of symbolic attackers and the benefits of unconditional soundness: the technique of the computationally complete symbolic attacker of Bana and Comon (BC) [8]. In this article, we argue that the real breakthrough of this technique is the recent introduction of its version for indistinguishability [9], because, with the extensions we introduce here, for the first time, there is a computationally sound symbolic technique that is syntactically strikingly simple, to which translating standard computational security notions is a straightforward matter, and that can be effectively used for verification of not only equivalence properties but trace properties of protocols as well. We first fully develop the core elements of this newer version by introducing several new axioms. We illustrate the power and the diverse use of the introduced axioms on simple examples first. We introduce an axiom expressing the Decisional Diffie-Hellman property. We analyze the Diffie-Hellman key exchange, both in its simplest form and an authenticated version as well. We provide computationally sound verification of real-or-random secrecy of the Diffie-Hellman key exchange protocol formultiple sessions, without any restrictions on the computational implementation other than the DDH assumption. We also show authentication for a simplified version of the station-to-station protocol using UF-CMA assumption for digital signatures. Finally, we axiomatize IND-CPA, IND-CCA1, and IND-CCA2 security properties and illustrate their usage. We have formalized the axiomatic system in an interactive theorem prover, Coq, and have machine-checked the proofs of various auxiliary theorems and security properties of Diffie-Hellman and station-to-station protocol.

  • Psychosocial Twin Cohort Studies in Japan: The Keio Twin Research Center (KoTReC)

    Ando J., Fujisawa K.K., Hiraishi K., Shikishima C., Kawamoto T., Nozaki M., Yamagata S., Takahashi Y., Suzuki K., Someya Y., Ozaki K., Deno M., Tanaka M., Sasaki S., Toda T., Kobayashi K., Sakagami M., Okada M., Kijima N., Takizawa R., Murayama K.

    Twin Research and Human Genetics (Twin Research and Human Genetics)  22 ( 6 ) 591 - 596 2019年12月

    ISSN  18324274

     概要を見る

    © The Author(s) 2020. The Keio Twin Research Center (KoTReC) was established in 2009 at Keio University to combine two longitudinal cohort projects - the Keio Twin Study (KTS) for adolescence and adulthood and the Tokyo Twin Cohort Project (ToTCoP) for infancy and childhood. KoTReC also conducted a two-time panel study of self-control and psychopathology in twin adolescence in 2012 and 2013 and three independent anonymous cross-sectional twin surveys (ToTcross) before 2012 - the ToTCross, the Junior and Senior High School Survey and the High School Survey. This article introduces the recent research designs of KoTReC and its publications.

全件表示 >>

KOARA(リポジトリ)収録論文等 【 表示 / 非表示

全件表示 >>

総説・解説等 【 表示 / 非表示

  • Corrigendum to “Inductive-data-type systems” [Theoret. Comput. Sci. 272 (1–2) (2002) 41–68] (Theoretical Computer Science (2002) 272(1–2) (41–68), (S0304397500003479), (10.1016/S0304-3975(00)00347-9))

    Blanqui F., Jouannaud J.P., Okada M.

    Theoretical Computer Science (Theoretical Computer Science)  817   81 - 82 2020年05月

    ISSN  03043975

     概要を見る

    © 2000 Elsevier B.V. In a previous work (Abstract data type systems, Theoret. Comput. Sci. 173 (2) (1997)), the last two authors presented a combined language made of a (strongly normalizing) algebraic rewrite system and a typed lambda-calculus enriched by pattern-matching definitions following a certain format, called the “General Schema”, which generalizes the usual recursor definitions for natural numbers and similar “basic inductive types”. This combined language was shown to be strongly normalizing. The purpose of this paper is to reformulate and extend the General Schema in order to make it easily extensible, to capture a more general class of inductive types, called “strictly positive”, and to ease the strong normalization proof of the resulting system. This result provides a computation model for the combination of an algebraic specification language based on abstract data types and of a strongly typed functional language with strictly positive inductive types.

  • Preface

    Nigam V., Kirigin T.B., Talcott C., Guttman J., Kuznetsov S., Loo B.T., Okada M.

    Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics))  12300 LNCS   vii - viii 2020年

    ISSN  03029743

  • FATALIS: Real Time Processes as Linear Logic Specifications

    Koji Hasebe, V. Cremet, Jean-Pierre Jouannaud, Antonie Kremer, and Mitsuhiro Okada

    International Workshop on Automated Verification of Infinite-State Systems  2003年

    総説・解説(その他), 共著

  • 歪んだ真珠(バロック)---音楽における規則性vs反規則性、または ロゴスvsパトス---

    岡田 光弘

    藝文研究  ( 9 )  2003年

    総説・解説(その他), 単著

  • 大会ワークショップ「フォーマルオントロジーの工学と哲学」報告

    日本科学哲学会   2002年

    その他記事, 単著

全件表示 >>

研究発表 【 表示 / 非表示

  • エシィクス・インテグリティ・義務論・法に関わるサイバーセキュリティの社会的インパクト

    岡田光弘、パネリスト

    第5回日仏サイバーセキュリティワークショップ (京都大学) , 2019年04月, シンポジウム・ワークショップ パネル(指名), 慶應義塾大学、NICT、駐日フランス大使館、INRIA,CNRS (ローカルオーガナイザー:京都大学)

  • normativity and rules

    岡田 光弘

    French-Japanese Meeting on Philosophy of Logic and Mathematics, "rule, Normativity and Disagreement" (慶應義塾大学) , 2019年01月, シンポジウム・ワークショップ パネル(指名), French-japanese CNRA-Keio U Project

  • Formal language and logic

    岡田光弘

    "Logic, Language and Ontology" Workshop (慶應義塾大学 三田キャンパス) , 2018年11月, 口頭(招待・特別), "Logic, Language and Ontology" Workshop Organizing Committee

  • Why "formal" is needed for algorithmic ethics?

    Mitsuhiro Okada

    French-Japanese Meeting for Algorithmic Fairness, 2018年10月, 口頭(一般)

  • A system of quasi-ordinal diagrams

    岡田 光弘-高橋優太

    The 20th International Workshop on Computation with Terms and Graphs (オックスフォード) , 2018年07月, シンポジウム・ワークショップ パネル(公募), TermGraph 2018 Program Committee

全件表示 >>

競争的資金等の研究課題 【 表示 / 非表示

  • 論証・証明の哲学の深化に向けた学際的「論理の哲学」研究

    2021年04月
    -
    2026年03月

    JSPS, 科学研究費 , 岡田光弘, 峯島宏次、 伊藤遼, 基盤研究(B)

  • 論理的「不一致」の解明

    2020年01月
    -
    2024年03月

    文部科学省・日本学術振興会, 科学研究費助成事業, 岡田 光弘, 国際共同研究加速基金(国際共同研究強化(B)), 補助金,  代表

  • 「証明の哲学」の視点に立つ「論理と数学の哲学」の新展開

    2017年04月
    -
    2022年03月

    日本学術振興会, 科学研究費補助金(文部科学省・日本学術振興会), 岡田光弘, 補助金,  代表

     研究概要を見る

    証明と論証の観点から、論理の哲学と数学の哲学の基本的諸問題を捉え直しています。

  • 論理的ー形式的手法による情報セキュリティ研究ー暗 号プロトコル検証と量的情報流解

    2016年04月
    -
    2019年03月

    日本学術振興会, 二国間共同研究 AYAMEプログラム, 岡田光弘, 受託研究,  代表

     研究概要を見る

    論理手法ー形式手法の情報セキュリティ研究への応用を行っている。時に、慶應義塾班では、暗号プロトコルの安全性の論理的・形式的証明を与えて、安全性を論理的に保証す論理のる手法を開発している。計算論と論理を繋ぐための、論理の計算論的健全性を与え、それをデフォルト推論の意味論にも応用しています。

  • 直観主義論理を中心とした学際的論理哲学研究

    2014年04月
    -
    2018年03月

    日本学術振興会, 科学研究費補助金(文部科学省・日本学術振興会), 岡田 光弘, 補助金,  代表

     研究概要を見る

    哲学・倫理学

     備考を見る

    基盤研究(B)

全件表示 >>

Works 【 表示 / 非表示

  • 飯田「ウィトゲンシュタイン」書評

    2000年
    -
    継続中

    その他, 単独

     発表内容を見る

    左記図書の書評

  • 公と私(石黒ひで氏との対談)

    1999年05月
    -
    継続中

    その他, 単独

     発表内容を見る

    左記テーマでの対談

  • 「脳と心のモデル(安西他著)」書評

    1994年
    -
    継続中

    その他, 単独

     発表内容を見る

    左記図書の書評

  • 大出「論理学入門」について

    1992年11月
    -
    継続中

    その他, 単独

     発表内容を見る

    左記図書についての書評

その他 【 表示 / 非表示

  •  内容を見る

    <書評>ウィトゲンシュタイン:言語の限界 飯田隆著, 講談社, 1997年. 哲學, 104:77-83, 1999年12月.

 

担当授業科目 【 表示 / 非表示

  • 現代論理学の諸問題Ⅱ

    2021年度

  • 現代論理学の諸問題Ⅰ

    2021年度

  • 計算論理学

    2021年度

  • 哲学倫理学特殊ⅡI

    2021年度

  • 哲学倫理学特殊ⅠI

    2021年度

全件表示 >>

 

社会活動 【 表示 / 非表示

  • 三田哲学会誌「哲学」

    1997年04月
    -
    2000年03月

所属学協会 【 表示 / 非表示

  • 竹内シンポジウム, 

    2003年12月
  • シンポジウム「意識研究」の学際的方法論を求めて, 

    2003年12月
    -
    継続中
  • 「数学と論理の哲学」ワークショップ, 

    2003年12月
  • 「ヒルベルト・ワークショップ」, 

    2002年01月
    -
    継続中
  • 日仏情報学ワークショップ(フランス外務省主催), 

    2001年12月
    -
    継続中

全件表示 >>

委員歴 【 表示 / 非表示

  • 2020年04月
    -
    継続中

    海外交流ディレクター, 科学基礎論学会

  • 2019年04月
    -
    継続中

    編集委員会委員長, 日本科学哲学会

  • 2019年01月
    -
    継続中

    大会実行委員会委員長, 日本科学哲学会

     特記事項を見る

    2018年大会委員長内定

  • 2017年04月
    -
    2020年03月

    理事会理事, 日本科学基礎論学会

  • 2017年04月
    -
    継続中

    理事会理事, 日本科学哲学会

全件表示 >>