Details of a Researcher - Okada, Mitsuhiro

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

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

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

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

2021.04

2026.03

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

論理的「不一致」の解明

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の論理」研究者達との研究協力の企画を行った。

モデルチェッキング法の限界を超える新しい論理的手法によるダイナミックな実時間システムのための検証ツールの実現

2001

Present

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

申請者がこれまでに確立した、線形論理に基づいた(有限状態)稠密実時間並行システムの仕様・検証の形式的体系に対する、(1)証明のPSPACE決定可能性と、(2)発展的実時間システムの検証に対する適応性と,(3)(表示的意味論に対する)完全性いう3つの結果を用いて、論理的手法による実時間システム検証の理論を完成させた。特に、我々の枠組みでは、ダイナミックな変化を許す進化的、発展的実時間システムの安全性、リアクティヴ性、種々のスケジュール問題の自動検証、解析が可能である。エージェントの数が増加したり(例えば、鉄道交通網のある状況のもとで臨時列車をダイヤに組み入れたり)、時間制約が動的に変化したり(例えば、ある条件のもとで締め切り時間の延期通告が出たり)ということは、現実の実時間システムでは日常的に起こり得るが、このようなダイナミックで現実的な実時間システムに応用できる論理的検証ツールをわれわれのこれまでの理論的成果に基づいて実現するための準備研究を行った。又、我々の論理的検証系は、一部に危険な状態が生じ得ることが分っている実時間システムのなかで、安全なスケジュールを自動的に探し出したり、与えられた条件を満たすスケジュールを自動的に探しだすことを可能とする。

フランス国立情報科学研究所と共同で申請者の理論の中核部分の実装試作を行ってきた。この試作された論理的検証系FATALIS Systemが来年度の日本側の上記実装研究の基盤として用いられる。

International collaborative studies on a logical specification and verification language.

2001

2003

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

We developed and designed a formal specification and verification tool for dynamic real-time systems in the collaboration with the French partner group (Jean-Pierre Jouannaud's group), based on linear logic. By dynamic real-time systems we mean a multi-agent systems in which the number of participating agents may be changed and the time constraints may be changed dynamically We gave an automated transformation procedure to transform a natural specification on the user-level into a linear logical specification. We also gave an elimination procedure to eliminate the dense time notions from a linear logical specification. Then, various kinds of verifications are performed in terms of the proof-search mechanism of a fragment of linear logic. The dense time elimination procedure is given by a program extraction method known in constructive logic. We also developed a logical framework for the security protocol correctness proofs, applying the same concept. We also studied some related logical research on our linear logic, which is the logical framework of our verification tool.

発展的実時間システムの自動検証を可能にする新しい論理的検証理論

2001

2002

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

本年度は、第1年次に開発した論理的理論を基にした仕様、検証の有効性を確かめ、仕様、検証の新しい論理的方法論を開発した。とくに、まず実時間システムの研究分野でベンチマークとして使われている代表的な実時間システムの具体例を発展的システムの例に変形し、これに我々の方法論を適用し、われわれの論理的な方法論とこれまでの他の方法論とを比較した。(例えば、今までの静的な交通網モデルを、新たに交通網が複雑化したり、電車の本数が変化したり、列車ダイヤの改定や時間制約の変化が起こったりする進化的モデルに作り変えて検討した。)

とくに、これまでのPVS言語やTLA言語などで代表されるような、伝統的な述語論理に基づいた論理的手法では、述語論理の表現力を用いて形式仕様が可能であるが、これらPVS言語やTLA言語の(および、その他の述語論理に基づく)枠組では、一般に証明可能性問題が非決定的であるため、形式的検証を体系的に遂行することができなかった。そこで彼らは、この言語使用者の責任において、与えられた形式仕様に特有な種々のInvariant Propertiesを見つけだし、それをもとに多重の数学的帰納法を適用して、検証の論理的証明を構成する、というアドホックな方法を採用していた。しかし現実の問題として、少し規模が大きな実時間システムを設計しようとすると、このような適当なInvariant Propertiesを一般の設計者自身が自分の責任で見いだすことは不可能であるのが実情である。これに対して、我々の線形論理に基づいた論理体系の枠組みは(PSPACE)決定可能であるので、仕様された実時間システムの安全性検証の証明構成(または危険性の証明構成)が自動的に遂行できる。この違いを具体的な例を用いて分析した。

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

2000

Present

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

特定領域研究「新しい論理学の展開」及びそれと並行して行う国際共同研究に向けて,その準備のための企画・調査を行った.現在進みつつある新しい論理学の展開を把握し,論理学の進むべき方向を明らかにしていくには,哲学系論理学者達が中心となり,これに西洋・東洋の論理学史の学者達および認知科学,言語学,人工知能論,情報科学基礎論,数学基礎論を含めて特定領域研究チームを形成する必要がある.このため,本企画・調査研究においても,論理哲学者だけでなく,これに認知言語学者,論理学史者,情報科学者に加わってもらった.

昨年度に引続き,岡田は論理哲学(数学基礎論やフッサール後期の論理学も含む)を,飯田は言語分析哲学を,野矢は日常言語と論理との関係を,土屋は認知科学的立場からの論理を,岩田はおもに印度論理を中心に企画調査を行った.また,これらのメンバーの各々は,哲学以外の他の分野との交流も盛んに行ってきた.例えば,土屋は言語学界および認知科学界においても哲学的立場から多くの成果をあげており,また岡田及び佐藤は人工知能論や情報科学や数学との境界領域の研究者達との打ち合わせも進めてきた.また,これまでも哲学系の研究代表者岡田と分担者土屋は情報科学系の分担者佐藤と分野を超えて本企画調査のための学術交流を重ねてきた.

これと並行して,岡田が海外における代表的な哲学系論理学の共同研究プロジェクトの視察・調査を行った.特に4月にソルボンヌ大(パリ大学第1校)哲学科において欧州側共同研究者達と共同研究企画のための会合を行ったのに続いて,7月末のヨーロッパ論理学会の折には米国側の共同研究者達も含めて上記課題の国際共同研究の企画会議を行った.

Safety Verification Technologies based on Behavioral Specifications

2000

2003

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

The following results have been gotten by doing research for developing the verification technology which is highly applicable and flexible, and is amenable for automation.

(1)Inspection Technology for Unknown Viruses : Based on the logics of behavioral specifications, a technology for modeling behavior s of programs and automatically inspecting their safety is developed. A virus inspection program is developed for Windows OS, and the effectiveness of developed technology has been proved.

(2) Safety Verification Technology based on Behavior Specification : By formalizing requirements and/or specifications in behavior level, a verification technology is developed which can verify the safety properties of systems in the level which is more honest to users or application logics. The technology has been applied to railway signal systems, software components, concurrent and distributed systems, and secure protocols, and is proved to be effective. In particular, verifications of several practical e-commerce protocols have been done using the technology.

(3) Model Checking Technology based on Behavioral Specification : Based on behavioral specifications, a model checking technology which is effective for software with infinite states is developed.

Theory of formal specification and verification of concurrency systems and real-time systems based on linear logic

2000

2002

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

We gave a logical method for formal specification and formal verification of concurrent systems, in particular real-time concurrent systems, which contains quantified time constraints in the dense-time setting.

In the first half of the project we gave a concrete algorithm for verification of the basic safety and other related properties (the membership property, the appointment property, the liveness property, etc.) in the dense real-time setting. We also gave a theory of automated transformation from a specification (written in the framework of natural description language) into a linear logical specification.

Then in the second half of the project we extended our theories to dynamic real-time systems where the number of agents/participants and the form of time-constraints are dynamically changed. We also compared our linear logical method with the traditional model checking and the timed automata method.

特定領域研究「新しい論理学の展開」のための企画研究

1999

Present

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

特定領域研究「新しい論理学の展開」に向けて、その準備のための企画・調査を行った。現在進みつつある新しい論理学の展開を把握し、論理学の進むべき方向を明らかにしていくには、哲学系論理学者達が中心となり、これに西洋・東洋の論理学史の学者達および認知科学、言語学、人工知能論、情報科学基礎論、数学基礎論を含めて特定領域研究チームを形成する必要がある。このため、本企画・調査研究においても、論理哲学者達だけでなく、これに認知言語学者、論理学史学者、情報科学者に加わってもらった。

岡田は論理哲学(数学基礎論やフッサール後期の論理学も含む)を、飯田は言語分析哲学を、野矢は日常言語と論理との関係を、土屋は認知科学的立場からの論理を、岩田はおもに印度論理を中心に企画調査を行った。また、これらのメンバーの各々は、哲学以外の他の分野との交流も盛んに行ってきた。例えば、土屋は言語学界および認知科学界においても哲学的立場から多くの成果をあげており、また岡田は人工知能論や情報科学や数学との境界領域の研究者たちとの打ち合わせも進めてきた。また、これまでも哲学系の研究代表者岡田と分担者土屋は情報科学系の分担者佐藤と分野を超えて本企画調査のための学術交流を重ねてきた。

これと並行して、岡田が海外における代表的な哲学系論理学の共同研究プロジェクトの視察・調査を行った。また、ソルボンヌ大学哲学科Joinet博士、パリ・エコールノルマールシュープリュールのLongo博士ら欧州の論理学者およびホンコン大学哲学科及び米国テキサス大哲学科Thomason博士らアジア、米国の何人かの分析哲学者や言語行為論の論理研究者らを招いて、本研究企画のためのディスカッションを行い、助言を仰いだ。

実時間システムの形式仕様・検証のための新しい論理的方法論

1999

2000

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

第2年次は,申請者がこれまでに確立した,線形論理に基づいた(有限状態)実時間並行システム仕様・検証の形式的体系に対する,証明のPSPACE決定可能性と(表示的意味論に対する)完全性という二つの定理を用いて,論理的手法による実時間システムの開発ツールを実装した.われわれのツールは次の特徴を持つ.

1.その第1は,ひとつの実時間システム全体の設計に伴う,システマティックな論理的形式仕様および,われわれの(PSPACE)決定手続きを用いた安全性・信頼性の自動検証が可能である.これは,これまでに得られた上記二つの論理的基本定理を用いることにより直接遂行できた.

2.その第2は,すでに与えられている実時間システムに新たな部分を加えたり,ある部分を変更したりするときに必要となる形式検証の問題や,二つの独立に作られた(安全性がそれぞれに対して保証されている)実時間システムを統合・総合しようとするときに必要となる形式検証の問題である.われわれの論理的な仕様・検証の枠組みは,もともと高度のモジュラー性を有しているので,このような問題に対しても本質的に上記1の方法論を応用することができた.

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

Logic of Knowledge Discovery

1998

2000

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

In our project project, we studied foundations of the logic of knowledge discovery and computation models of knowledge discovery.

In our study of foundations of the logic of knowledge discovery, we aimed to give such foundations from the two sides of logic in philosophy and mathematical logic, and we studied the 'context of discovery', in particular, discoveries which cannot be reduced to logical algorithms. Furthermore, we stuidied deductive aspects of logic of discovery from the standpoint of mathematcial and formal loigc. Also, we analyzed the process of acquiring knolwedge and concepts in disccovery from the philosophical standpoint, and we formalized it base on a theory of belief revsion. Moreover, we studied the relationship between the introduction of ideal concepts in mathematics and discovery in mathematcis, and we gave foudations for the study of discovery of new concepts.

In our study on computaion models of konwledge discovery, we studied computaion models corresponding to logic of knowledge discovery, and implemented several systems which realize appropriate computation models. In pariticular, we obtained results in (I) a computation model for solving problems in distributed compatation space, (ii) discovery of algorithms by model checking method and (iii) algorithm discovery porcedure from proofs in classical logic.

　 Previous page - Next page 　