2016 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 |
矛盾許容論理、時間論理、適切論理、確率論理、構成的論理などのいくつかを組み合わせたり拡張したりする方法を提案した。それら論理に対してカット除去定理および完全性定理を証明した。これらの結果およびここまでの研究結果をまとめて、ジャーナル論文9本および国際会議論文2本として出版した。
特に以下の論文[1]では、適切論理と矛盾許容論理を組み合わせた拡張を提案しカット除去定理と完全性定理を証明した。以下の論文[2]では、時間論理、矛盾許容論理および確率論理を組み合わせた拡張を提案し、その論理を用いたモデル検査に対する決定可能性を示した。以下の論文[3]では、構成的論理の変種と矛盾許容論理を組み合わせた拡張を提案し、完全性定理を証明した。
論文：[1] N. Kamide, A decidable paraconsistent relevant logic: Gentzen system and Routley-Meyer semantics, Mathematical Logic Quarterly 62 (3), 2016.[2] N. Kamide and D. Koizumi, Method for combining paraconsistency and sequentiality in temporal reasoning, Journal of Advanced Computational Intelligence and Intelligent Informatics 20 (5), 2016. [3] N. Kamide and H. Wansing, Completeness of connexive Heyting-Brouwer logic, IFCoLog Journal of Logics and their Applications 3 (3), 2016.
|
| 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]では、時間論理、矛盾許容論理および確率論理を適切に組み合わせた拡張論理に対するモデル検査の決定可能性を証明することができた。また、同論文では提案した論理のモデル検査への応用も提案することができた。
論文：[1] N. Kamide, Bunched sequential information, Journal of Applied Logic 15, 2016.[2] N. Kamide, A decidable paraconsistent relevant logic: Gentzen system and Routley-Meyer semantics, Mathematical Logic Quarterly 62 (3), 2016.[3] N. Kamide and D. Koizumi, Method for combining paraconsistency and sequentiality in temporal reasoning, Journal of Advanced Computational Intelligence and Intelligent Informatics 20 (5), 2016. [4] N. Kamide and H. Wansing, Completeness of connexive Heyting-Brouwer logic, IFCoLog Journal of Logics and their Applications 3 (3), 2016.
|
| Strategy for Future Research Activity |
今後は、量子論理と矛盾許容論理を組み合わせた矛盾許容量子論理の拡張を考察する予定である。そのような拡張として、時間論理と矛盾許容量子論理を組み合わせた時間矛盾許容量子論理や、無限論理と矛盾許容量子論理を組み合わせた無限矛盾許容量子論理を提案する予定である。また、これら2つの拡張を組み合わた無限時間矛盾許容量子論理を構築する予定である。これら論理のカット除去定理を証明し、時間矛盾許容量子論理については決定可能性を証明する予定である。また、これら論理に対してクリプキ型の意味論を構築し、それらに対する完全性定理を証明する予定である。さらに、これら拡張論理をベースにした集合論を構築しそれらの性質を明らかにする予定である。
ここまでに得られた結果および、これから得られる結果を、以下のような国際会議およびジャーナルで発表する予定である。また、これまでの結果をまとめることにより、埋め込み定理を基にした証明手法の非古典論理への応用に関する著書を1冊執筆する予定である。
国際会議：[1] IEEE International Symposium on Multiple-Valued Logic (ISMVL). [2] International Conference on Agents and Artificial Intelligence. [3] International Workshop on Logic, Rationality, and Interaction.
ジャーナル：[1] Journal of Philosophical Logic. [2] Journal of Logic and Computation.[3] Mathematical Logic Quarterly.
|
| Causes of Carryover |
職務の都合等により、予定していた国際会議への出席を取りやめたため、129,463円の未使用金が残った。
|
| Expenditure Plan for Carryover Budget |
平成29年度は複数の国際会議に出席する予定である。そのため、平成28年度からの繰り越し金129,463円と併せてそれら会議への出席のために使用する予定である。すでに2017年5月に開催される国際会議IEEE International Symposium on Multiple-Valued Logic (ISMVL 2017)への出席が決まっており、会議開催国であるセルビアへの交通費として約20万円を立て替えで支払っている。これに加えて、2017年9月に開催される国際会議International Conference on Knowledge-Based and Intelligent Information & Engineering Systems (KES 2017)への出席も決まっている。
|
