2015 Fiscal Year Research-status Report
Project/Area Number |
26330263
|
Research Institution | Teikyo University |
Principal Investigator |
上出 哲広 帝京大学, 理工学部, 准教授 (60332053)
|
Project Period (FY) |
2014-04-01 – 2019-03-31
|
Keywords | 矛盾許容論理 / 時間論理 / 完全性定理 / カット除去定理 / シーケント計算 / モデル検査 |
Outline of Annual Research Achievements |
矛盾許容論理と時間論理を融合した矛盾許容時間論理を構築し、その理論基盤を整備するとともに新たな応用を提案した。理論基盤の整備としては、論理の基本的な性質を表すいくつかの重要な定理を証明した。応用としては、矛盾許容推論と時間依存推論を組み合わせた推論の形式化を提案した。そのような推論の具体的適用例として、学習支援システムや医療診断システムを検証するためのモデル検査アルゴリズムを開発した。 提案した論理は、標準的な矛盾許容論理と時間論理を組み合わせることによって構築した。提案した論理の統語論としては、シーケント計算を採用した。意味論としては、クリプケ意味論を採用した。以上で構築した統語論および意味論に対して、完全性定理、カット除去定理、決定可能性、等を証明した。これらを証明するにあたって、埋め込み定理を使用した効率的かつシンプルな統一的証明手法を開発した。 上記の結果およびこれまでの研究結果をまとめて、ジャーナル論文5本および国際会議論文4本として出版することができた。特に、以下の論文[1]では、矛盾許容論理と時間論理を融合した矛盾許容時間論理の、モデル検査技術への応用を提案した。論文[2]では、矛盾許容論理に対する埋め込み定理を用いた手法を提案した。 [1] Norihiro Kamide, Inconsistency-tolerant temporal reasoning with hierarchical information, Information Sciences 320, pp. 140-155, 2015. [2] Norihiro Kamide, Trilattice logic: An embedding-based approach, Journal of Logic and Computation 25 (3), pp. 581-611, 2015.
|
Current Status of Research Progress |
Current Status of Research Progress
2: Research has progressed on the whole more than it was originally planned.
Reason
当初予定していた、拡張論理の応用を提案することができた。それら結果を、以下の論文として出版することができた。当初の予定では応用に関する研究は、来年度以降としていた。しかしながら、本年度中に一部ではあるが完了することができた。 [1] Norihiro Kamide, Inconsistency-tolerant temporal reasoning with hierarchical information, Information Sciences 320, pp. 140-155, 2015. [2] Norihiro Kamide, Reasoning in medical and tutoring systems: A decidable first-order temporal paraconsistent non-commutative logic, International Journal of Software and Informatics 9 (1), pp. 73-92, 2015, The Institute of Software, Chinese Academy of Sciences (ISCAS). [3] Norihiro Kamide, A decidable temporal relevant logic for time-dependent relevant human reasoning,Proceedings of the 5th International Workshop on Logic, Rationality, and Interaction (LORI 2015), Lecture Notes in Computer Science 9394, pp. 182-194, 2015.
|
Strategy for Future Research Activity |
今後は、ここまでに考察してきた矛盾許容論理(paraconsistent logics)や時間論理(temporal logics)とは異なるタイプの論理体系について分析する予定である。矛盾許容の一種である多重束論理(multilattice logics)について考察を進める予定である。多重束論理は、我々がこれまで研究してきた二重束(bilattice logics)や三重束(trilattice logics)の一般化であり、ほとんど研究されていない。時間論理については無限論理(infinitary logic)の拡張となるような無限時間論理(infinitary temporal logics)について研究する予定である。また、これら矛盾許容論理と時間論理を融合した新たな論理体系を研究する予定である。 ここまでに得られた結果および、これから得られる結果を、以下のようなジャーナルおよび国際会議で発表する予定である。また、これまでの結果をまとめることにより、埋め込み定理を基にした証明手法の非古典論理への応用に関する著書を1冊執筆する予定である。 ジャーナル:[1] Journal of Applie Logic. [2] Journal of Logic and Computation. [3] Journal of Applied Non-Classical Logics. [4] Mathematical Logic Quarterly. 国際会議:[1] International Conference on Agents and Artificial Intelligence. [2] International Workshop on Logic, Rationality, and Interaction. [3] International Conference on Logic for Programming, Artificial Intelligence and Reasoning (LPAR). [4] Automated Reasoning with Analytic Tableaux and Related Methods (TABLEAUX).
|
Research Products
(14 results)