2016 Fiscal Year Research-status Report
多次元・多ソート化によるエージェント相互作用の証明論的研究
| Project/Area Number |
15K21025
|
|---|
| Research Institution | Hokkaido University |
|---|
Principal Investigator |
佐野 勝彦 北海道大学, 文学研究科, 准教授 (20456809)
|
|---|
| Project Period (FY) |
2015-04-01 – 2018-03-31
|
| Keywords | チーム意味論 / 様相論理 / 動的認識論理 / 信念と知識の論理 / ハイブリッド論理 / 証明論 |
|---|
| Outline of Annual Research Achievements |
本課題には、(A) エージェント構造と信念変化の相互作用の形式化, (B) 不確実性下の信念・知識の論理, (C) 情報伝達行為の証明論的研究, の3つの課題が存在した。以下3つに分けて本年度の研究実績の概要を説明する。(A) については、信頼性構造と信念構造の両方をD.ルイスの球系 (systems of spheres) で捉え、こういった二つの構造の相互作用について語ることが可能な二次元ハイブリッド論理を提案し、国際会議SOCREAL 2017において招待講演を行った。またこれとは独立に Sujata Ghosh (ISI Chennai)と協力し、エージェントの信頼性構造と信念構造の相互作用をとらえる論理的枠組みを構築し、ICAART2017で発表した。(B)に関しては、研究協力者のJonni Virtema と共同で昨年度に引き続き, 一つの状況・世界ではなく，それらの集まりの上で論理式を評価する様相論理のTeam 意味論に関して、依存関係を表す原子式を加えた様相論理の構文論がクリプキ構造に対してもつ表現力をクリプキ構造のクラスを制限することでさらに調べた (Wollic 2016に採択)。(C) については、北陸先端大 博士課程学生 秦野亮と共同で van Benthem and Liu による関係変化子をもつ動的論理に対するラベル付き計算体系を与え、健全性・完全性・カット除去定理を証明し、国際ワークショップAWPL-TPLC2016 で発表を行った。また Seligman らによる Epistemic Logic of Friendship に対する式計算体系を与え、カット除去定理・健全性・完全性を示した上で、未解決であったEpistemic Logic of Friendshipの健全かつ完全となるヒルベルト式公理系を見出した。この結果については2017年度に開催される国際会議LORI6へ投稿した。
|
| Current Status of Research Progress |
Current Status of Research Progress
1: Research has progressed more than it was originally planned.
Reason
申請時の予定通り、本年度は、既存研究を踏まえた信頼性構造と信念変化に関する課題(A) と関係変化のラベル付き証明体系に関する課題(C) にまず取り組んだが、準備的議論が十分にできていたため、２つの課題に関して一定の成果を挙げることができた。
|
| Strategy for Future Research Activity |
昨年度に引き続き、本年度も準備的議論が十分にできていたため、当初の計画以上に研究を進展させることができた。申請当初の予定に従えば、残っている研究トピックは「チャネル理論の多ソート論理」「Team 意味論によるDEL」 である。前者については、本年度の関係変化のラベル付き証明体系に関する課題(C)との重要な関連を見出すことができたので、研究協力者との議論により研究の推進が見込める。後者については2017年度に研究協力者のJonni Virtema 氏を日本へ招へいし集中的に研究打ち合わせを行う予定である。
|
| Causes of Carryover |
次年度使用額が生じたのは、2016年度9月に研究機関の移動があり、2016年度後半に当初予想したよりも多くの講義を担当する必要があり、当初の予定以上に国内・海外出張に行くことができなかったためである。
|
| Expenditure Plan for Carryover Budget |
本年度に進めた研究成果を国内・海外で発表するため、また研究協力者との研究打ち合わせのための出張・招へい費用として利用する予定である。
|
