Theory and applications of non-classical logics

2022 Fiscal Year Final Research Report

• 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: Kamide Norihiro 帝京大学, 理工学部, 准教授 (60332053)
• Project Period (FY): 2018-04-01 – 2023-03-31
• 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.

Free Research Field

論理学

Academic Significance and Societal Importance of the Research Achievements

本研究で提案したような拡張非古典論理に対する基礎理論は, 従来の応用分野を拡張する. そして「矛盾状態を考慮した実用的な推論」を適切に扱えるような, 矛盾許容モデル検査技術, 矛盾許容定理証明システム, 矛盾許容論理プログラミング言語などに対する厳密な理論的正当化を与え, それら技術をコンピュータ上へ実装することの正当性を保証する. また, 本研究で提案する埋め込み定理を基にした手法の開発は, 論理学における重要課題の一つである「論理の組み合わせ問題」への解決策の一つになり得る. 提案した拡張モデル検査技術を用いることによって, モデル検査技術を臨床推論検証へ応用することが可能になった.