| Project/Area Number |
23K10990
|
|---|
| 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 | Nagoya City University |
|---|
Principal Investigator |
上出 哲広 名古屋市立大学, データサイエンス学部, 教授 (60332053)
|
|---|
| Project Period (FY) |
2023-04-01 – 2028-03-31
|
| Project Status |
Granted (Fiscal Year 2023)
|
| Budget Amount *help |
¥2,600,000 (Direct Cost: ¥2,000,000、Indirect Cost: ¥600,000)
Fiscal Year 2027: ¥520,000 (Direct Cost: ¥400,000、Indirect Cost: ¥120,000)
Fiscal Year 2026: ¥520,000 (Direct Cost: ¥400,000、Indirect Cost: ¥120,000)
Fiscal Year 2025: ¥520,000 (Direct Cost: ¥400,000、Indirect Cost: ¥120,000)
Fiscal Year 2024: ¥520,000 (Direct Cost: ¥400,000、Indirect Cost: ¥120,000)
Fiscal Year 2023: ¥520,000 (Direct Cost: ¥400,000、Indirect Cost: ¥120,000)
|
|---|
| Keywords | 矛盾許容論理 / 埋め込み定理 / 完全性定理 / カット除去定理 / シーケント計算 / 様相論理 / 非古典論理 / 時間論理 / 確率論理 / ファジー論理 |
|---|
| Outline of Research at the Start |
本研究では, 矛盾許容性, 曖昧性及び不確実性を考慮した拡張非古典論理の基礎理論を構築するとともにその応用を提案する. 本研究で対象とする拡張非古典論理は, 矛盾許容論理, ファジー論理, 確率論理, 時間論理, 記述論理などの非古典論理を組み合わせた拡張である. 本研究では, 研究代表者らが開発してきた「埋め込み定理を用いた証明手法」を基にして, 当該拡張非古典論理に対するカット除去定理, 完全性定理, 決定可能性定理, 補間定理などを統一的に扱うことが可能な基礎理論を構築する. さらに, 構築した基礎理論を用いた拡張推論技術への応用を提案する.
|
| Outline of Annual Research Achievements |
2023年度は、矛盾許容性を考慮した拡張非古典論理に対する研究成果を得た[1, 2, 3]。特に論文[1]では、線形時間論理に対するシーケント計算体系のカット除去定理と完全性定理に関する結果を得た。論文[2]では、標準的な様相論理に対するシーケント計算体系のカット除去定理と完全性定理に関する結果を得た。論文[3]では、構成的論理の一種であるGurevich論理に対する埋め込み定理に関する結果を得た。特に、この論文では、ゲーデル・ゲンツェン変換に基づいた、古典論理からGurevich論理への埋め込み定理を証明した。
論文: [1] N. Kamide, Refutation-aware Gentzen-style calculi for propositional until-free linear-time temporal logic, Studia Logica 111 (6), pp. 979-1014, 2023. [2] N. Kamide, Falsification-aware calculi and semantics for normal modal logics including S4 and S5, Journal of Logic, Language and Information 32 (3), pp. 395-440, 2023. [3] N. Kamide, Embedding first-order classical logic into Gurevich's extended first-order intuitionistic logic: the role of strong negation, Journal of Applied Logics 10 (6), pp. 1025-1058, 2023.
|
| Current Status of Research Progress |
Current Status of Research Progress
2: Research has progressed on the whole more than it was originally planned.
Reason
2013年度は、3編のジャーナル論文及び2編の国際会議論文を出版した。特に論文[1]では、線形時間論理に対するシーケント計算体系のカット除去定理と完全性定理に関する結果を得た。論文[2]では、標準的な様相論理に対するシーケント計算体系のカット除去定理と完全性定理に関する結果を得た。論文[3]では、構成的論理の一種であるGurevich論理に対する埋め込み定理に関する結果を得た。特に、この論文では、ゲーデル・ゲンツェン変換に基づいた、古典論理からGurevich論理への埋め込み定理を証明した。現在、Gurevich論理に関する研究を継続している。
論文: [1] N. Kamide, Refutation-aware Gentzen-style calculi for propositional until-free linear-time temporal logic, Studia Logica 111 (6), pp. 979-1014, 2023. [2] N. Kamide, Falsification-aware calculi and semantics for normal modal logics including S4 and S5, Journal of Logic, Language and Information 32 (3), pp. 395-440, 2023. [3] N. Kamide, Embedding first-order classical logic into Gurevich's extended first-order intuitionistic logic: the role of strong negation, Journal of Applied Logics 10 (6), pp. 1025-1058, 2023.
|
| Strategy for Future Research Activity |
2024年度は、引き続き矛盾許容性を考慮した拡張非古典論理に対する研究を推進する予定である。特に、それら拡張非古典論理と古典論理及び様相論理との対応関係に着目した埋め込み定理を証明することに注力する予定である。具体的には、様相論理S4からGurevich論理への埋め込み定理（ゲーデル・マッキンゼイ・タルスキ定理の変種）を証明する予定である。さらに、それら埋め込み定理を用いることにより、カット除去定理、正規化定理、完全性定理、補間定理及び決定可能性定理を証明する方法を検討する予定である。さらに、これまで考慮してこなかった各種拡張非古典論理に対しても同様に埋め込み定理を証明することを検討している。そのような対象となる拡張非古典論理の具体例として、Connexive論理の変種を検討している。
ここまでに得られた結果及びこれから得られる結果を、論理学およびコンピュータサイエンスの国際雑誌である Studia Logica、Journal of Logic, Language and Information、Journal of Logic and Computation、Journal of Philosophical Logic などで発表する予定である。また、ここまでに得られた結果およびこれから得られる結果を、国際会議である Non-Classical Logics: Theory and Application、IEEE International Symposium on Multiple-Valued Logic (ISMVL)及び International Conference on Agents and Artificial Intelligence (ICAART)などで発表する予定である。
|
