2021 Fiscal Year Annual Research Report
A proof-theoretic study of distributed knowledge
| Project/Area Number |
21J10573
|
|---|
| Research Institution | Hokkaido University |
|---|
Principal Investigator |
村井 涼 北海道大学, 文学研究院, 特別研究員(PD)
|
|---|
| Project Period (FY) |
2021-04-28 – 2023-03-31
|
| Keywords | 分散知識 / 認識論理 / 様相論理 / シークエント計算 / 証明論 |
|---|
| Outline of Annual Research Achievements |
(1)直観主義的な知識概念のBHK解釈を与えた研究としてArtemovとProtopopescuによる直観主義認識論理が知られている。蘇有安氏及び佐野勝彦氏とともにこの論理に分散知識概念を導入する研究に取り組み、国際会議LORI 2021のプロシーディング論文として研究結果を投稿し受理された。本共同研究においては、筆者は主に完全性定理に関わる技術的な貢献を行った。
(2)佐野勝彦氏との共著論文が雑誌Computacion y Sistemasから2022年に出版された。この論文では、(1)の研究とは異なる発想で直観主義論理を基盤とする分散知識論理を考案し、その完全性定理を示したほか、カット除去定理の成り立つシークエント計算を構築し、カット除去定理を利用してクレイグ補間定理と決定可能性を証明した。
(3)佐野勝彦氏との共著論文が2023年3月に雑紙Studia Logicaに受理された。この論文では、(2)の論文の論理体系を拡張して、直観主義論理を基盤とした、分散知識概念を持つ公開告知論理を考案し、その完全性定理を示した。
(4)2019年度の研究と(2)(3)の研究をもとに博士論文を執筆・提出し、審査に合格した。
(5)2019年度の佐野勝彦氏との共同研究において、古典論理上の種々の分散知識論理に対するシークエント計算が得られていた。これらの中にはカット除去定理が成り立たないものが複数あるが、そのうちのいくつかについては部分論理式特性が成り立つことを、従来基本的な様相論理に対して用いられていた意味論的な手法を応用して証明した。さらに、そのうち認識論理研究において重要な三つの論理のシークエント計算については証明論的な手法を用いることで部分論理式特性からクレイグ補間定理が帰結することを示した。本結果を2023年3月に第57回MLG数理論理学研究集会で発表した。
|
| Current Status of Research Progress |
Current Status of Research Progress
2: Research has progressed on the whole more than it was originally planned.
Reason
国際雑誌論文の投稿と博士論文の提出を行うことができた。
|
| Strategy for Future Research Activity |
古典論理上の種々の分散知識論理に対するシークエント計算について、従来基本的な様相論理に対して用いられていた意味論的な手法を適用して部分論理式特性が証明できるかを検討する。
|
