2021 Fiscal Year Research-status Report
非古典論理の基礎理論とそのコンピュータサイエンスへの応用
| Project/Area Number |
18K11171
|
|---|
| Research Institution | Teikyo University |
|---|
Principal Investigator |
上出 哲広 帝京大学, 理工学部, 准教授 (60332053)
|
|---|
| Project Period (FY) |
2018-04-01 – 2023-03-31
|
| Keywords | 矛盾許容論理 / 埋め込み定理 / 完全性定理 / カット除去定理 / モデル検査 |
|---|
| Outline of Annual Research Achievements |
基礎理論に関する研究では、反証的意味論・証明システムに関する結果と拡張矛盾許容論理に関する結果を得た[1, 2]。特に[1]では、反証的意味論・証明システムを提案し、それらと従来の意味論・証明システムとの同等性を証明した。また、[2]では、直観主義的矛盾許容論理に対して、カット除去定理、完全性定理および補間定理を簡単に証明する方法を示した。応用に関する研究では、[3]において、上記[1]の枠組みをモデル検査技術に適用する方法を示した。
論文: [1] N. Kamide, Falsification-aware semantics and sequent calculi for classical logic, Journal of Philosophical Logic 51, 2022. [2] N. Kamide, Cut-elimination, completeness, and Craig interpolation theorems for Gurevich's extended first-order intuitionistic logic with strong negation, Journal of Applied Logics 8 (5), 2021. [3] N. Kamide and S. Kanbe, Falsification-aware semantics for CTL and its inconsistency-tolerant subsystem: Towards falsification-aware model checking, Proceedings of the 14th International Conference on Agents and Artificial Intelligence, 2022.
|
| Current Status of Research Progress |
Current Status of Research Progress
2: Research has progressed on the whole more than it was originally planned.
Reason
本年度は、3編のジャーナル論文および4編の国際会議論文を出版した。特に[1]では、新たに反証的意味論・証明システムを提案した。[2]では、直観主義的矛盾許容論理に対する基本定理を簡単に証明する方法を与えた。[3]では、反証的意味論のモデル検査技術への応用を提案した。このモデル検査の応用技術を反証的モデル検査と名付けた。現在、反証的モデル検査技術の応用に関する研究を継続している。
論文: [1] N. Kamide, Falsification-aware semantics and sequent calculi for classical logic, Journal of Philosophical Logic 51, pp. 99-126, 2022. [2] N. Kamide, Cut-elimination, completeness, and Craig interpolation theorems for Gurevich's extended first-order intuitionistic logic with strong negation, Journal of Applied Logics 8 (5), pp. 1101-1122, 2021. [3] N. Kamide, S. Kanbe, Falsification-aware semantics for CTL and its inconsistency-tolerant subsystem: Towards falsification-aware model checking, Proceedings of the 14th International Conference on Agents and Artificial Intelligence, pp. 242-252, 2022.
|
| Strategy for Future Research Activity |
理論関連では引き続き反証的意味論・証明システムの枠組みを様相論理や時間論理の拡張に適用する研究を継続する予定である。応用関連では、反証的モデル検査の枠組みを拡張し、不確定性および曖昧性（ファジネス）も同時に扱える枠組みを構築する予定である。また、これまで考慮してこなかった非古典論理に対しても埋め込み定理を証明する方法を開発する予定である。
ここまでに得られた結果およびこれから得られる結果を, 論理学およびコンピュータサイエンスの国際雑誌であるStudia Logica, Journal of Logic, Language and Information, Journal of Logic and Computation, Journal of Philosophical Logicなどで発表する予定である. また、ここまでに得られた結果およびこれから得られる結果を, インターネット上で開催される国際会議であるThe 52nd IEEE International Symposium on Multiple-Valued Logic (ISMVL 2022), the 15th International Conference on Agents and Artificial Intelligence (ICAART 2023), the 8th International Conference on Fuzzy Systems and Data Mining (FSDM 2022)などで発表する予定である。
|
