A proof-theoretic study of distributed knowledge

(1)2021年度に雑誌Computacion y Sistemasに受理されていた、受入研究者の佐野勝彦氏との共著論文"Intuitionistic Epistemic Logic with Distributed Knowledge"が出版された。この論文では、古典論理ではなく直観主義論理を基盤とする分散知識論理を考案し、その完全性定理を示したほか、カット除去定理の成り立つシークエント計算を構築し、カット除去定理を利用した証明論的な手法を用いてクレイグ補間定理と決定可能性を証明した。(2)2021年度に雑誌Studia Logicaに投稿していた佐野勝彦氏との共著論文"Intuitionistic Public Announcement Logic with Distributed Knowledge"が2022年度に行った修正を経て2023年3月に受理された。この論文では、(1)の論文の論理体系を拡張して、直観主義論理を基盤とした、分散知識概念を持つ公開告知論理を考案し、その完全性定理を示している。(3)2019年度の佐野勝彦氏との研究において、古典論理上の種々の分散知識論理に対するシークエント計算が得られていた。これらの中にはカット除去定理というシークエント計算における重要な定理が成り立たないものが複数あるが、そのうちのいくつかについては部分論理式特性という良い性質が成り立つことを、従来基本的な様相論理に対して用いられていた意味論的な手法を応用して証明した。さらに、そのうち$\mathbf{S5}_D$, $\mathbf{K45}_D$, $\mathbf{KD45}_D$の三つについては証明論的な手法を用いることで部分論理式特性からクレイグ補間定理が帰結することを示した。本結果を2023年3月に第57回MLG数理論理学研究集会で発表した。

(1)2021年度に雑誌Computacion y Sistemasに受理されていた、受入研究者の佐野勝彦氏との共著論文"Intuitionistic Epistemic Logic with Distributed Knowledge"が出版された。この論文では、古典論理ではなく直観主義論理を基盤とする分散知識論理を考案し、その完全性定理を示したほか、カット除去定理の成り立つシークエント計算を構築し、カット除去定理を利用した証明論的な手法を用いてクレイグ補間定理と決定可能性を証明した。(2)2021年度に雑誌Studia Logicaに投稿していた佐野勝彦氏との共著論文"Intuitionistic Public Announcement Logic with Distributed Knowledge"が2022年度に行った修正を経て2023年3月に受理された。この論文では、(1)の論文の論理体系を拡張して、直観主義論理を基盤とした、分散知識概念を持つ公開告知論理を考案し、その完全性定理を示している。(3)2019年度の佐野勝彦氏との研究において、古典論理上の種々の分散知識論理に対するシークエント計算が得られていた。これらの中にはカット除去定理というシークエント計算における重要な定理が成り立たないものが複数あるが、そのうちのいくつかについては部分論理式特性という良い性質が成り立つことを、従来基本的な様相論理に対して用いられていた意味論的な手法を応用して証明した。さらに、そのうち$\mathbf{S5}_D$, $\mathbf{K45}_D$, $\mathbf{KD45}_D$の三つについては証明論的な手法を用いることで部分論理式特性からクレイグ補間定理が帰結することを示した。本結果を2023年3月に第57回MLG数理論理学研究集会で発表した。