Details of a Researcher - Okada, Mitsuhiro

Research Projects of Competitive Funds, etc. - Okada, Mitsuhiro

Division display 1 - 20 of about 29 ／ All the affair displays >>

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

2021.04

2026.03

JSPS, 科学研究費　, Mitsuhiro Okada, Koji Mineshima, Ryo Ito, 基盤研究(B), No Setting

Interdisciplinary studies on philosophy of logic: Toward the development of philosophy of proof and demonstration

2021.04

2026.03

MEXT,JSPS, Grant-in-Aid for Scientific Research, Grant-in-Aid for Scientific Research (B), Principal investigator

論理的「不一致」の解明

2020.01

2024.03

MEXT,JSPS, Grant-in-Aid for Scientific Research, Fund for the Promotion of Joint International Research (Home-Returning Researcher Development Research (B)), Principal investigator

A New Development of "Philosophy of Logic and Mathematics" from the view point of "Philosophy of Proofs"

2017.04

2022.03

JSPS, Grant-in-Aid for Scientific Research, Mitsuhiro OKADA, Research grant, Principal investigator

Information security research based on logical-formal methods-cruptographic protocols quantitative information flow analysys

2016.04

2019.03

JSPS, AYAME-Program (JSPS-INRIA), Mitsuhiro OKADA, Commissioned ｒesearch, Principal investigator

Interdisciplinary study on logical philosophy based on intuitionistic logic

2014.04

2018.03

JSPS, Grant-in-Aid for Scientific Research, OKADA, Mitsuhiro, Research grant, Principal investigator

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

2014.04

2017.03

JSPS, 科学研究費, 基盤研究(B), No Setting

Logic and computation for prediction, judgment and decision making

2011.07

2016.03

JSPS, Grant-in-Aid for Scientific Research, OKADA, Mitsuhiro, Research grant, Principal investigator

論理哲学の学際研究ー直観主義論理の推論・証明理論を中心として

2011.04

2015.03

日本学術振興会, Grant-in-Aid for Scientific Research, OKADA, Mitsuhiro, Principal investigator

前年度に引き続き、直観主義論理を中心とした現代論理学的研究を行った。直観主義論理と古典論理を含む論理の一元論的捉え方について、線形論理的手法と観点を拡張することを通じて検討し、成果を挙げた。このことを証明論、論理的意味論の両面から考察し、またその両者を融合する見方を与えた。

フッサール、ヒルベルト学派、ウィトゲンシュタインを中心とした論理哲学の研究を進め、直観主義論理と古典論理との関係について新しい哲学的知見を得た。特に等式算術証明体系に対してフッサールとウィトゲンシュタインが２０世紀初めに果たした前駆的な役割について新たな解明の手掛かりを与えた。フッサールの論理哲学とヒルベルトの論理哲学の関係や相違について研究を進めた。まら、ウィトゲンシュタインと英国構成主義論理学者グッドシュタインの論理哲学上の影響関係について考察を進めた。

図形的表現による論理推論証明体系について、直観主義論理的図形推論と古典論理的図形推論の区別を特徴付ることに成功した。

以上の成果を基に、認知科学的観点から直観主義論理と古典論理の推論プロセスモデルを検討した。特にこれまで認知心理学分野でなされてきた論理推論の先行研究を我々の立場から批判的に検討した。

直観主義論理と古典論理の関係についての新しい我々の視点に立ってコーエン流のForcingモデル構成（またはFitting-Ono流のモデル構成）を捉え直し、

一種の認識論理的枠組みに適用して、情報科学分野の情報通信モデル（特に通信プロトコル安全性）の計算論的完全性の問題に応用した。

Logical inference research by combining logic, cognitive acience and genetics

2006.04

2008.03

JSPS, Grant-in-Aid for Scientific Research, Mitsuhiro OKADA, Research grant, Principal investigator

Behavioral genetic study in adolescence and adulthood by twin method

2006

2009.03

日本学術振興会, Grant-in-Aid for Scientific Research, ANDO, Juko, Research grant, Coinvestigator(s)

800組の青年・成人期の双生児を対象とした行動遺伝学的研究から、認知能力、パーソナリティなどの遺伝・環境構造の解明を行った。一般知能の遺伝的実在性、社会的適応に及ぼす内的環境適応の過程、パーソナリティの普遍的遺伝構造モデルの提案、自尊心感情の縦断的変化などが成果としてなされた。また双生児データのデータベース化、webによる双生児調査フレームワークの確立もなされた。

論理学・認知科学・遺伝学を統合した論理推論研究

2006

2007

日本学術振興会, Grant-in-Aid for Scientific Research, OKADA, Mitsuhiro, Research grant, No Setting

1)線形論理や種々の新しい論理学理論の立場から、伝統的な認知科学的理論推論モデルや理論哲学的論理推論モデルの批判的分析や改訂を行った。特に、メンタルモデル理論とメンタルロジック理論に関する認知心理学の古典的論争やシンタクスとセマンティクスに関する論理哲学、情報科学等における二元論を現代論理学的観点から見直した。2)これまでは比較的少数の被験者調査を行うのが常であったが、統計的手法による実証的なデータ解析による大規模調査の方法論の研究を行った。「Baroco論理推論課題集」と呼ばれる演繹推論標準課題集を本申請グループが開発してきたが、これをさらに改良した。この課題集を用いて通常のIQ課題の関連性や、図形的表現による論理推論と言語的理論推論の(パフォーマンス)比較、抽象的推論と内容的推論の比較、信念相反的推論や領域依存的推論、論証構成と反例検索などに関わるデータの分析を行った。白血球中のRNAの転写量の差を調べるという方法論を導入することによって認知能力の関連遺伝子の所在とその効果量について調査する方法論を開発した。

Provably Secure Software Technology and Its Applications with the Special Focus on Smart Card and GRID Applications

2005.03

2009.03

JST, Strategic International Research Cooperative Program, Mitsuhiro OKADA, Principal investigator

モデルチェッキング法の限界を超えるダイナミック実時間システムのための論理的検証法

2004

2006

日本学術振興会, Grant-in-Aid for Scientific Research, OKADA, Mitsuhiro, Research grant, Principal investigator

我々の研究の枠組は論理的推論や演繹の方法論を用いて、ロジカル・リーズニングを実時間システムの構築等の形式仕様・形式検証に取り入れようとする点に(例えば伝統的モデルチェッキング法やオートマタ理論的分析と違った)最大の特徴がある。

我々の方法論がダイナミックな変化を許す進化的、発展的実時間システム特有の検証、解析に対して有効であることを示した。また、神戸大学田村研究室グループからの協力も得て、我々の理論の実装を論理型プログラム言語上で進めた。これまでの理論的研究と実装的研究の統合も行った。

論理的形式検証の方法論を認証プロトコルの安全性検証にも応用してきた。認証プロトコルの論理的検証においても、attackersの参入や新しい認証子の発行等のようなシステムのダイナミックな変化を捉える方法論を確立することが重要である。昨年度の準備研究の成果を踏まえて、protocol logicsの論理的分析を中心として、論理的検証の方法論の具体的応用を与えた。

また、特に、認証プロトコルのagreement properties検証に関するprotocol logicの基本部分を一階述語論理上で再構成し、その完全性定理及び反例生成系を与えた。この理論の応用のための反例生成系の実装試作も行った。認証プロトコルの安全性検証に関する実時間解析の手法の研究も進めた。

モデルチェッキング法の限界を超えるダイナミック実時間システムのための論理的検証法

2003

Present

日本学術振興会, Grant-in-Aid for Scientific Research, OKADA, Mitsuhiro, Research grant, Principal investigator

線形論理に基づいた(有限状態)実時間並行システム仕様・検証の形式的体系に対する我々のこれまでの成果をもとにして、論理的手法による実時間システム検証の理論の研究を進めた。我々の論理的検証理論は、次のような特徴を持つものとなる。

1.体系的で論理的な形式仕様の方法論及び、実時間システムの安全性・リアクティヴ性、種々のスケジューリング問題等の自動検証の方法論である。

2.ダイナミックな変化を許す進化的、発展的実時間システム特有の検証、解析に対する有効性である。エージェントの数が増加したり時間制約が動的に変化したりするような、ダイナミックで現実的な実時間システムに応用できる論理的検証ツールが実現できる。

3.一部に危険な状態が生じ得ることが分かっている実時間システムのなかで、システムの仕様にどのような手直しをすれば安全になるかを我々の論理的推論体系を用いて分析するツールの開発である。

又、我々の理論の実装にあたっては、フランス側INRIA-LRI-LIXグループとともに論理的形式仕様・検証言語Coq-System上で行なった実装試作を基盤として用いた。実装試作は日本側(岡田)が我々の理論的成果に基づいて検証手続の基本部分の具体的アルゴリズムを理論から抽出して進められた。この実装作業はCoq-グループの2人の大学院生により進められた。岡田-Jouannaudが共同指導教員となりこの作業を進めている。研究協力者神戸大田村グループと論理型言語を使った実装も行なった。又、この新しい方法論の実践的な応用を目的にした研究(特に、実践的な実時間制約や時刻認証を含んだ枠組での認証プロトコルのセキュリティ分析など)の準備を行なった。このために認証プロトコルの論理的検証理論や通信プロトコルの時間制約の論理的分析についての研究を進めた。

日米科学協力事業「ソフトウェア検証の論理的方法」更新のための企画研究

2003

Present

日本学術振興会, Grant-in-Aid for Scientific Research, OKADA, Mitsuhiro, Principal investigator

これまでの日米共同研究の成果を基にして平成15年度にこの日米共同研究プロジェクトを発展的に継続すべく研究計画の企画を日米間で行った。米国側は本年より同様な企画のため、若い世代に中核メンバーを移行しながら日米共同研究の更新の準備を開始しており、日本側も本企画研究の遂行過程で若手世代に移行していく計画を進めた。現在までは日本側は岡田(慶応大)が、又米国側はScedrov(ペンシルバニア大)、Mitchell(スタンフォード大)が幹事役として共同研究や共同主催国際会議の企画を行い、これら幹事役と同世代の研究者達が井同研究の中核となってきた。(過去3年間に3回の日米ワークショップ及び特定領域「安全」グループ(代表:米澤教授(東大))と連携したソフトウェア安全性に関する国際シンポジウムを開催し、Theoretical Computer Science誌特別号、States-of-Art Series of LNCS (Springer)等を編集し、日米共同研究の成果発表も行ってきた。)今回の企画研究ではこれらの成果やこれまでの共同研究体制を分析し、今後の改良点を検討した。米国側からScedrov、Cervesato、Nuclaらが秋に来日し今後の共同研究の企画立案を行った。特にソフトウェア及びネットワークコミュニケーションの安全性検証のための共同研究の方法論を検討した。我々のソフトウェア検証の論理的方法についての日米共同研究は欧州やカナダ等の研究グループの研究とも深く関連するため、これらの研究グループとも打合せをして我々の研究企画に役立てた。

New development in the matured linear logic research and its applications

2003

2005

日本学術振興会, Grant-in-Aid for Scientific Research, OKADA, Mitsuhiro, Research grant, Principal investigator

Linear logical proof theory and semantics theory have been developed and the researches have reached a matured stage to integrate proof theory and semantics theory. In this project we developed a method of integrating proof theory and semantics of linear logic and related logics.

We specially developed a method to study proof theoretic properties using this integrated framework, by using a phase semantic techniques, including the relation between "simple logic" and linear logic, uniform and abstract characterizations of cut-eliminations and logical computation models.

We also applied the linear logical syntax and semantics to formal verification techniques on real-time system designs and correctness proof techniques on security protocols as well as to computational complexity theory and type-inference theories for programming languages.

特定領域研究及び国際共同研究「新しい論理学の展開」のための企画研究

2002

Present

日本学術振興会, Grant-in-Aid for Scientific Research, OKADA, Mitsuhiro, Research grant, Principal investigator

特定領域研究及び国際共同研究「新しい論理学の展開」に向けた企画・調査を行った。本企画・調査研究班は、論理哲学者達だけでなく、これに認知言語学者、論理学史学者、情報科学者等も含めて形成されている。特に本年度は国際共同研究の基礎となるネットワーク作りを発展させた。

(1)企画にあたっては英米系論理哲学の分野だけでなく、認知科学・情報科学・AIなどとの学際的分野や、西洋・東洋論理哲学史や現象学的論理学をはじめ広い意味での論理の哲学的解明に関わる分野も視野に入れて進めた。又、我々哲学系論理学グループが中心となり、これに情報科学系AI及び認知科学系、数学基礎論系研究者達を交えてオントロジー工学、現象学的論理学、線形論理学等の分野を中心に学際的企画研究を進めた。

(2)哲学系論理学グループを中心に欧州及び北米の研究グループとの協議を進め、欧州グループおよび北米グループとも協力して特定領域研究を立ち上げるための調査を進めた。なお、欧米の企画グループGirard及びJoinet及びAbrusciとは欧州の論理哲学界との研究協力の企画を行った。Benoistらとは各々のグループと現象学的論理学の共同研究企画を行った。又北米の論理学者達との間でも調査を進め、特にScedrov.Mitchell等の北米の重要な論理学グループが来日して協議を行った。

モデルチェッキング法の限界を超えるダイナミック実時間システムのための論理的検証法

2002

Present

日本学術振興会, Grant-in-Aid for Scientific Research, OKADA, Mitsuhiro, Research grant, No Setting

論理的手法による実時間システム検証の理論を情報学的観点から完成させることを本研究課題の目的としている。又この理論の実装に関して現れる情報学的問題を研究してきた。次のような特徴を持つ論理的検証系の理論を構築してきた。

その第1は、実時間システム全体の設計に伴う、体系的で論理的な形式仕様の方法論および、実時間システムの安全性・リアクティヴ性、種々のスケジューリング問題等の自動検証の方法論の開発である。これまでに得られた我々の論理的検証系に対するPSPACE決定性定理を応用してこの方法論を開発してきた。

その第2は、ダイナミックな変化を許す進化的、発展的実時間システム特有の検証、解析に対する有効性の検討である。エージェントの数が増加したり、時間制約が動的に変化したり(例えば、ある条件のもとで締め切り時間の延期通告が出たり)ということは、現実の実時間システムでは日常的に起こり得るが、このようなダイナミックで現実的な実時間システムに応用できる論理的検証ツールの方法論の開発を進めた。

その第3は、一部に危険な状態が生じ得ることが分っている実時間システムのなかで、ある具体的なプラン(プロセスのスケジュール)が安全であるかどうかをわれわれの論理的推論体系を用いて分析するツールの方法論の開発である。論理推論体系を(通常、定理自動証明の分野で行われているように)ボトムアップ的に用いると、我々の完全性定理を適用することにより、論理的に証明できない命題に対しては、その反例がシステマティックに生成される。この論理推論体系の持つ基本的なメカニズムを危険な状態を示す命題に対して適用すると、その反例となるプロセススケジュール(プラン)、即ち安全なブロセススケジュール(プラン)の具体例が自動的に生成・枚挙される手続きが得られるのである。この考え方に基づいて、与えられた実時間システム内での種々のプラニングの問題の論理的な分析ツールの方法論を開発した。

国際共同研究及び特定領域研究「新しい論理学の展開」のための企画研究課題番号：13891001

2001

Present

日本学術振興会, Grant-in-Aid for Scientific Research, OKADA, Mitsuhiro, Research grant, Principal investigator

特定領域研究及び国際共同研究「新しい論理学の展開」に向けた企画・調査を行った。本企画・調査研究班は、論理哲学者達だけでなく、これに認知言語学者、論理学史学者、情報科学者含めて形成されている。各々の分担者が各自の専門分野を担当する形で、特定領域研究の企画を進めた。

1.企画にあたっては英米系論理哲学の分野だけでなく、認知科学・情報科学・AIなどとの学際的分野や、西洋・東洋論理哲学史や現象学的論理学をはじめ広い意味での論埋の哲学的解明に関わる分野も視野に入れて進めた。本チームメンバー(および研究協力者グループ)との研究会を重ねて各分野から出された共同研究の企画を検討した。又、我々哲学系論理学グループが中心となり、これに情報科学系AI及び認知科学系、数学基礎論系研究者達を交えて「哲学と工学におけるオントロジー」ワークショップ、「ヒルベルト」国際ワークショップ、「ウィトゲンシュタインの数学の哲学」ワークショップ等多数の研究会を行い、学際的企画研究を進めた。

2.哲学系論理学グループを中心に欧州及び北米の研究グループとの協議を進め、欧州グループおよび北米グループのそれぞれの地域での研究費申請と連動して、日本側も特定領域研究を立ち上げるための準備を進めた。なお、欧米の企画グループvan Dalen及びJoinet及びAbrusciとは欧州の論理哲学界との研究協力の企画を行った。Benoistとは各々のグループと現象学的論理学の共同研究企画を行った。Girard及びBarendregtとは欧州の惰報論理学界との共同研究企画を行った。Mancosu及びZach及びDrummondとは北米論理哲学界との共同研究の企画を行った。Vandervekenとは北米の言語行為論者達および「AIの論理」研究者達との研究協力の企画を行った。

　 Previous page - Next page 　