| 研究課題/領域番号 |
15300008
|
|---|
| 研究種目 |
基盤研究(B)
|
| 配分区分 | 補助金 |
|---|
| 応募区分 | 一般 |
|---|
| 研究分野 |
ソフトウエア
|
|---|
| 研究機関 | 慶應義塾大学 |
|---|
研究代表者 |
岡田 光弘 慶應義塾大学, 文学部, 教授 (30224025)
|
|---|
| 研究分担者 |
小林 直樹 東北大学, 大学院・情報科学研究科, 教授 (00262155)
照井 一成 国立情報学研究所, 助手 (70353422)
田村 直之 神戸大学, 学術基盤研究センター, 教授 (60207248)
|
|---|
| 研究期間 (年度) |
2003 – 2005
|
| 研究課題ステータス |
完了 (2005年度)
|
| 配分額 *注記 |
11,500千円 (直接経費: 11,500千円)
2005年度: 3,700千円 (直接経費: 3,700千円)
2004年度: 3,700千円 (直接経費: 3,700千円)
2003年度: 4,100千円 (直接経費: 4,100千円)
|
|---|
| キーワード | 論理的手法 / 線形論理 / 形式仕様 / 形式検証 / 実時間システム / 証明論 |
|---|
| 研究概要 |
次の3点を中心に研究を進めた。
1.証明論と意味論の統合的見方について研究を進めた。カット消去定理等の証明論の基本定理の成立条件がPhase semanticsによる意味論的分析により明らかになることを示した。又、Simple logic等の線形論理の基礎理論に対して、証明論と意味論の統合を進めた。さらに、直観主義論理Phase semanticsと古典論理Phase semanticsとの密接な関係を明らかにした。Phase semanticsの成果に基づいてカット消去定理の意味論的条件の研究を進めた。
2.Reduction Paradigmによる計算モデルとProof-Search Paradigmによる計算モデルを統一的に分析できる論理的枠組の確立に向けた研究を進めた。ゲーム論的意味論等の観点からの分析も加えた。(岡田・Girard等フランスグループとの共同研究)これまでのReduction Paradigm(関数型言語の論理計算モデル)とProof-Search Paradigm(論理型言語や証明構成の計算モデル)の内的な統合を可能にするLudics等の新たな論理体系理論の分析をGirardグループらと共同で行なった。
3.線形論理的概念がプログラミング言語理論やソフトウェア形式仕様・検証理論、計算量理論等にどのように応用され得るかのケーススタディーを行なった。例えば昨年に引き続き、ダイナミック実時間システムのシステマティックな設計・検証や認証プロトコル安全性証明等を例にとり、線形論理的観点や手法の応用可能性を示した。この目的でフランス及び米国共同研究グループとの共同研究を行なうとともに、計3回の成果報告会を日仏共同で行った。
|
