Project/Area Number |
18K11171
|
Research Category |
Grant-in-Aid for Scientific Research (C)
|
Allocation Type | Multi-year Fund |
Section | 一般 |
Review Section |
Basic Section 60010:Theory of informatics-related
|
Research Institution | Teikyo University |
Principal Investigator |
|
Project Period (FY) |
2018-04-01 – 2023-03-31
|
Project Status |
Completed (Fiscal Year 2022)
|
Budget Amount *help |
¥2,600,000 (Direct Cost: ¥2,000,000、Indirect Cost: ¥600,000)
Fiscal Year 2022: ¥520,000 (Direct Cost: ¥400,000、Indirect Cost: ¥120,000)
Fiscal Year 2021: ¥520,000 (Direct Cost: ¥400,000、Indirect Cost: ¥120,000)
Fiscal Year 2020: ¥520,000 (Direct Cost: ¥400,000、Indirect Cost: ¥120,000)
Fiscal Year 2019: ¥520,000 (Direct Cost: ¥400,000、Indirect Cost: ¥120,000)
Fiscal Year 2018: ¥520,000 (Direct Cost: ¥400,000、Indirect Cost: ¥120,000)
|
Keywords | 非古典論理 / 矛盾許容論理 / 時間論理 / 完全性定理 / カット除去定理 / モデル検査技術 / 埋め込み定理 / モデル検査 |
Outline of Final Research Achievements |
In this study, we construct a basic theory of non-classical logics and develop some computer science applications of the proposed theory. The logics considered in this study include inconsistency-tolerant logics, temporal logics, infinitary logics, substructural logics, quantum logics, and their combined extensions. We propose a unified embedding-based method for proving the cut-elimination, completeness, decidability theorems for the logics under consideration. Furthermore, we develop some model checking and theorem proving technologies based on the proposed theory.
|
Academic Significance and Societal Importance of the Research Achievements |
本研究で提案したような拡張非古典論理に対する基礎理論は, 従来の応用分野を拡張する. そして「矛盾状態を考慮した実用的な推論」を適切に扱えるような, 矛盾許容モデル検査技術, 矛盾許容定理証明システム, 矛盾許容論理プログラミング言語などに対する厳密な理論的正当化を与え, それら技術をコンピュータ上へ実装することの正当性を保証する. また, 本研究で提案する埋め込み定理を基にした手法の開発は, 論理学における重要課題の一つである「論理の組み合わせ問題」への解決策の一つになり得る. 提案した拡張モデル検査技術を用いることによって, モデル検査技術を臨床推論検証へ応用することが可能になった.
|