| 研究課題/領域番号 |
15K21025
|
|---|
| 研究機関 | 北陸先端科学技術大学院大学 |
|---|
研究代表者 |
佐野 勝彦 北陸先端科学技術大学院大学, 情報科学研究科, 助教 (20456809)
|
|---|
| 研究期間 (年度) |
2015-04-01 – 2018-03-31
|
| キーワード | Team 意味論 / 様相論理 / 公開告知論理 / 動的認識論理 / 信念と知識の論理 / 証明論 |
|---|
| 研究実績の概要 |
本課題には、(A) エージェント構造と信念変化の相互作用の形式化, (B) 不確実性下の信念・知識の論理, (C) 情報伝達行為の証明論的研究, の3つの課題が存在した。以下3つに分けて研究実績の概要を説明する。(A) については、研究協力者の北陸先端大 博士後期課程学生 Pimolluck Jirakunkanok, 及び, 東条敏教授と共同で、Lorini et al. 2011の既存研究で扱えなかった信頼性構造の変化を捉える動的演算子を提案し、裁判官の信念変化の論理的分析を行った。(B)に関しては、まず研究協力者のJonni Virtema と共同で次の2つのトピックに取り組んだ。一つの状況・世界ではなく，それらの集まりの上で論理式を評価する様相論理のTeam 意味論に関して、依存関係を表す原子式を加えた様相論理の構文論がクリプキ構造に対してもつ表現力を調べ(Wollic 2015に採択)、さらに依存関係を表す原子式を加えた様相論理（やその他の拡張）に対してタブロー計算とヒルベルト式公理系による公理化を初めて与えた(CSL 2015に採択)。さらに(B)については、東条敏教授と共同で告知内容のタイプ（許可か命令か）に対する誤解を許容する信念更新の論理についても成果を挙げた(KSE2015に採択)。(C) については、まずクリプキ構造上の多次元ハイブリッド論理に対して式計算体系を与え、LENLS12で研究発表を行った。
次に研究協力者の北陸先端大 博士後期課程学生 野村尚新、東条敏教授と共同で、既存研究の不備を正した公開告知論理(PAL)のラベル付き式計算体系を与え、カット除去定理・完全性・健全性を証明した。この研究成果で得た知見を直観主義的公開告知論理、動的認識論理へも活かし、こういった2つの論理に対してもラベル付き式計算体系を与えた(それぞれLPAR2015, LFCS2016に採択)。
|
| 現在までの達成度 (区分) |
現在までの達成度 (区分)
1: 当初の計画以上に進展している
理由
当初の予定通り、本年度（平成27年度）は、既存研究を踏まえた信頼性構造と信念変化に関する課題(A) と，公開告知論理(PAL) の証明体系に関する課題(C) にまず取り組んだが、準備的議論が十分にできていたため、初期の段階で２つの課題に関して一定の成果を挙げることができた。そのため、次年度以降に予定していた上記3つの課題の個別研究についてもさらに研究を進めることができた。
|
| 今後の研究の推進方策 |
本年度（平成27年度）は準備的議論が十分にできていたため、当初の計画以上に研究を進展させることができた。申請当初の予定に従えば、残っている研究トピックは「関係変化のラベル付き証明体系」、「チャネル理論の多ソート論理」、「Team 意味論によるDEL」, 「信頼性構造と信念変化（多次元版）」であるが、本年度の成果に基づいて進展が見込める「関係変化のラベル付き証明体系」と「信頼性構造と信念変化（多次元版）」に優先的に取り組む予定である。
|
| 次年度使用額が生じた理由 |
次年度使用額が生じたのは次の2つの理由からである。第一に、本年度には当初の予定よりも研究の進展が見込めたため、研究成果を挙げることに集中し、研究発表のために国内・海外出張に行くことを当初の予定よりも減らした。また、第二に、当初の計画では本年度に計算機購入予定であったが、本年度の研究状況では既存の計算機の性能で十分であったため、購入を控えた。
|
| 次年度使用額の使用計画 |
次年度使用額は、本年度に進めた研究成果を国内・海外で発表するため、ないし研究協力者との議論のための出張費用として利用する。また、本年度に購入することができなかった計算機の購入にも次年度使用額の一部をあてる予定である。
|
