本研究室では、人間の推論を研究する学問である「論理学」を基にした「推論に関する科学・工学」を教育・研究課題としています。論理学は主に以下の3つの分野に分けられます。
（1）情報科学・工学に現れる推論の基礎としての情報論理学。
（2）推論の数学的な構造を研究する数理論理学。
（3）推論を哲学的な視点から捉える哲学的論理学。
本研究室では、これら3つの分野のうち、特に（1）の情報論理学の教育・研究に中心的に取り組んでいます。情報論理学の観点から、人工知能・ソフトウェア科学・理論計算機科学に現れる「推論にかかわる課題」に取り組んでいます。また、上記（2）（3）の分野に関連する課題にも幅広く取り組んでいます。
基本情報
| 教員名・所属 | 上出哲広 / 理工学部情報電子工学科 |
|---|---|
| 専門分野 | 論理学、理論計算機科学、ソフトウェア科学、人工知能 |
| 研究テーマ | 論理学とその情報科学への応用に関する研究 |
| 研究キーワード | 知識表現、推論、非古典論理 |
| 教員紹介URL | https://www3.med.teikyo-u.ac.jp/profile/ja.1714ebd9c9e1c2a5.html |
研究紹介
モデル検査の基礎と応用に関する研究
モデル検査は、ソフトウェアおよびハードウェアの検証技術です。同技術は、2007年度のチューリング賞の受賞対象となった技術であり、時間論理を応用した技術です。本研究では、同技術の拡張や新たな応用分野の創出を目的としています。特に、矛盾許容性を適切に扱うことが可能なモデル検査の拡張である矛盾許容モデル検査や、階層性を適切に記述可能なモデル検査の拡張である階層モデル検査などについて研究しています。これら拡張されたモデル検査技術の新たな応用として、ソフトウェア検証分野での応用だけではなく、人工知能分野への応用も模索しています。
知識推論システムの論理的基礎付けに関する研究
知識表現と推論は、人工知能分野における最も重要な研究課題の一つです。例えば、これらは、インターネットを構成する基盤技術の一つであるwebオントロジー言語の開発に必要となるものです。本研究では、知識表現と推論を組み合わせたシステムである知識推論システムの論理的基礎付けに取り組んでいます。特に、webオントロジー言語の基礎として使用されている記述論理の拡張や変種を構成し、それらを用いた知識推論システムの効率の良い構成法を模索しています。より表現力が高くかつ効率的な知識推論システムを構成するための方法を模索しています。
非古典論理の研究
非古典論理とは、通常の数学で使用されている標準的な古典論理以外の論理の総称です。非古典論理の具体例としては、様相論理、矛盾許容論理、部分構造論理、量子論理、無限論理および構成的論理などが挙げられます。本研究では、これら非古典論理に対する基本的な性質を明らかにする研究を行っています。そのような基本的な性質を表す定理として、完全性定理、カット除去定理、正規化定理、埋め込み定理および補間定理などがあります。本研究では、これら定理を証明するための簡単な方法や新しい定理を得るための新たな証明法などを開発しています。
論文発表・学会発表
論文発表
| 題名 | 雑誌名 | 研究室 | 内容 |
|---|---|---|---|
| Cut-elimination, completeness, and Craig interpolation theorems for Gurevich's extended first-order intuitionistic logic with strong negation | Journal of Applied Logics 8 (5), pp. 1101-1122, College Publications, 2021. | 上出哲広 研究室 | 詳細 |
| Modal and intuitionistic variants of extended Belnap--Dunn logic with classical negation | Journal of Logic, Language and Information 30(3), pp. 491-531, Springer, 2021. | 上出哲広 研究室 | 詳細 |
| Alternative multilattice logics: An approach based on monosequent and indexed monosequent calculi | Studia Logica, Published online first, Springer, 2021. | 上出哲広 研究室 | 詳細 |
| Notes on Avron's self-extensional four-valued paradefinite logic | Proceedings of the 51st IEEE International Symposium on Multiple-Valued Logic (ISMVL 2021), pp. 43-49, IEEE Press, 2021. | 上出哲広 研究室 | 詳細 |
| Symmetric paraconsistent quantum logic | Proceedings of the 51st IEEE International Symposium on Multiple-Valued Logic (ISMVL 2021), pp. 26-32, IEEE Press, 2021. | 上出哲広 研究室 | 詳細 |
| Falsification-aware semantics and sequent calculi for classical logic | Journal of Philosophical Logic, Published online first, Springer, 2021. | 上出哲広 研究室 | 詳細 |
| Inconsistency-tolerant hierarchical probabilistic CTL model checking: Logical foundations and illustrative examples | International Journal of Software Engineering and Knowledge Engineering 32 (1), pp. 131-162, World Scientific, 2022. | 上出哲広研究室 | 詳細 |
| Reasoning with inconsistency-tolerant fuzzy description logics | Proceedings of the 14th International Conference on Agents and Artificial Intelligence (ICAART 2022), Volume 3, pp. 63-74, Science and Technology Publications, 2022. | 上出哲広研究室 | 詳細 |
| Falsification-aware semantics for CTL and its inconsistency-tolerant subsystem: Towards falsification-aware model checking | Proceedings of the 14th International Conference on Agents and Artificial Intelligence (ICAART 2022), Volume 3, pp. 242-252, Science and Technology Publications, 2022. | 上出哲広研究室 | 詳細 |
| 題名 | 雑誌名 | 研究室 | 内容 |
|---|---|---|---|
| Completeness and cut-elimination for first-order ideal paraconsistent four-valued logic | Studia Logica 108 (3), pp.549-571, Springer, 2020. | 上出哲広 研究室 | 詳細 |
| Kripke-completeness and cut-elimination theorems for intuitionistic paradefinite logics with and without quasi-explosion | Journal of Philosophical Logic, Online first, Springer, 2020. | 上出哲広 研究室 | 詳細 |
| Modal extension of ideal paraconsistent four-valued logic and its subsystem | Annals of Pure and Applied Logic, Online first, Elsevier, 2020. | 上出哲広 研究室 | 詳細 |
| Sequential fuzzy description logic: Reasoning for fuzzy knowledge bases with sequential information | Proceedings of the 50th IEEE International Symposium on Multiple-Valued Logic (ISMVL 2020), pp. 218-223, IEEE Press, 2020. | 上出哲広 研究室 | 詳細 |
| Completeness of subtrilattice logic | Proceedings of the 50th IEEE International Symposium on Multiple-Valued Logic (ISMVL 2020), pp.279-284, IEEE Press, 2020. | 上出哲広 研究室 | 詳細 |
| Lattice logic, bilattice logic and paraconsistent quantum logic: A unified framework based on monosequent systems | Journal of Philosophical Logic, Online first, Springer, 2021. | 上出哲広 研究室 | 詳細 |
| Inconsistency-tolerant hierarchical probabilistic computation tree logic and its application to model checking | Proceedings of the 13th International Conference on Agents and Artificial Intelligence (ICAART 2021), Volume 2, pp. 490-499, Science and Technology Publications, 2021. | 上出哲広 研究室 | 詳細 |
| 題名 | 雑誌名 | 研究室 | 内容 |
|---|---|---|---|
| Completeness and cut-elimination for first-order ideal paraconsistent four-valued logic | Studia Logica, Online first published, Springer, 2019. | 上出哲広 研究室 | 詳細 |
| Finite model property for modal ideal paraconsistent four-valued logic | Proceedings of the 49th IEEE International Symposium on Multiple-Valued Logic (ISMVL 2019), pp. 120-125, IEEE Press, 2019. | 上出哲広 研究室 | 詳細 |
| First-order Nelsonian paraconsistent quantum logic | Proceedings of the 49th IEEE International Symposium on Multiple-Valued Logic (ISMVL 2019), pp. 176-181, IEEE Press, 2019. | 上出哲広 研究室 | 詳細 |
| Bi-classical connexive logic and its modal extension: Cut-elimination, completeness and duality | Logic and Logical Philosophy 28 (3), pp. 481-511, Nicolaus Copernicus University Press, 2019. | 上出哲広 研究室 | 詳細 |
| A substructural view of multilattice logic | Journal of Multiple-Valued Logic and Soft Computing 33 (3), pp. 239-270, Old City Publishing, 2019. | 上出哲広 研究室 | 詳細 |
| Logical foundation of locative inconsistency-tolerant hierarchical probabilistic model checking | Abstract proceedings of the 5th International Conference on Fuzzy Systems and Data Mining (FSDM 2019), pp. 15-16, 2019. | 上出哲広 研究室 | 詳細 |
| Some properties of first-order Nelsonian paraconsistent quantum logic | Journal of Applied Logics - The IfCoLoG Journal of Logics and their Applications 7 (1), pp. 59-88, College Publications, 2020. | 上出哲広 研究室 | 詳細 |
| An extended description logic for inconsistency-tolerant ontological reasoning with sequential information | Proceedings of the 12th International Conference on Agents and Artificial Intelligence (ICAART 2020), Volume 2, pp. 313-321, Science and Technology Publications, 2020. | 上出哲広 研究室 | 詳細 |
| 題名 | 雑誌名 | 研究室 | 内容 |
|---|---|---|---|
| Proof theory of paraconsistent quantum logic | Journal of Philosophical Logic 47 (2), pp. 301-324, Springer, 2018. | 上出哲広 研究室 | 詳細 |
| Decidable temporal and sequential relevant logics | Journal of Logic and Computation 28 (2), pp. 403-432, Oxford University Press, 2018. | 上出哲広 研究室 | 詳細 |
| Yet another paradefinite logic: The role of conflation | Logic Journal of the IGPL, Published online first, Oxford University Press, 2018. | 上出哲広 研究室 | 詳細 |
| Logical foundations of hierarchical model checking | Data Technologies and Applications, 52(4), pp. 539-563, Emerald Publishing, 2018. | 上出哲広 研究室 | 詳細 |
| Extending paraconsistent quantum logic: A single-antecedent/succedent system approach | Mathematical Logic Quarterly, Wiley-vch Verlag, Published online first, 2018. | 上出哲広 研究室 | 詳細 |
| Foundations of Hierarchical Model Checking: Logics, Translations, and Examples | Abstract Proceedings of the 4th International Conference on Fuzzy Systems and Data Mining, Rangsit University Press, pp. 14-15, 2018. | 上出哲広 研究室 | 詳細 |
| Bi-classical connexive logic and its modal extension: Cut-elimination, completeness and duality | Logic and Logical Philosophy, Nicolaus Copernicus University Press, Published online first, 2019. | 上出哲広 研究室 | 詳細 |
| Gentzen-type sequent calculi for extended Belnap-Dunn logics with classical negation: A general framework | Logica Universalis, Springer, Published online first, 2018. | 上出哲広 研究室 | 詳細 |
| Foundations of inconsistency-tolerant model checking: Logics, translations, and examples | Agents and Artificial Intelligence, 10th International Conference ICAART 2018 Revised Selected Papers, Lecture Notes in Artificial Intelligence 11352, pp. 1-31, Springer, 2019. | 上出哲広 研究室 | 詳細 |
| An extended paradefinte Belnap-Dunn logic that is embeddable into classical logic and vice versa | Proceedings of the 11th International Conference on Agents and Artificial Intelligence (ICAART 2019), Volume 2, pp. 377-387, Science and Technology Publications, 2019. | 上出哲広 研究室 | 詳細 |
| Towards hierarchical probabilistic CTL model checking: Theoretical foundations | Proceedings of the 11th International Conference on Agents and Artificial Intelligence (ICAART 2019), Volume 2, pp. 762-769, Science and Technology Publications, 2019. | 上出哲広 研究室 | 詳細 |
| Towards locative inconsistency-tolerant hierarchical probabilistic CTL model checking: Survey and future work | Proceedings of the 11th International Conference on Agents and Artificial Intelligence (ICAART 2019), Volume 2, pp. 869-878, February 19-21, Science and Technology Publications, 2019. | 上出哲広 研究室 | 詳細 |
| 題名 | 雑誌名 | 研究室 | 内容 |
|---|---|---|---|
| Logics with definitional reflection rules | Journal of Logic and Computation 27 (5), pp. 1523-1548, Oxford University Press, 2017. | 上出哲広研究室 | 詳細 |
| Embedding from multilattice logic into classical logic and vice versa | Journal of Logic and Computation 27 (5), pp. 1549-1575, Oxford University Press, 2017. | 上出哲広研究室 | 詳細 |
| Phase semantics for multilattice formalism | Proceedings of the 47th IEEE International Symposium on Multiple-Valued Logic (ISMVL 2017), pp. 31-36, IEEE Press, 2017. | 上出哲広研究室 | 詳細 |
| Extending ideal paraconsistent four-valued logic | Proceedings of the 47th IEEE International Symposium on Multiple-Valued Logic (ISMVL 2017), pp. 49-54, IEEE Press, 2017 | 上出哲広研究室 | 詳細 |
| Natural deduction for connexive paraconsistent quantum logic | Proceedings of the 47th IEEE International Symposium on Multiple-Valued Logic (ISMVL 2017), pp. 207-212, IEEE Press, 2017. | 上出哲広研究室 | 詳細 |
| Modal multilattice logic | Logica Universalis 11(3), pp. 317-343, Springer, 2017. | 上出哲広研究室 | 詳細 |
| An extended first-order Belnap-Dunn logic with classical negation | Lecture Notes in Computer Science 10455, pp. 79-93, Springer, 2017. | 上出哲広研究室 | 詳細 |
| Logics and translations for hierarchical model checking | Procedia Computer Science 112, pp. 31-40, Elsevier, 2017. | 上出哲広研究室 | 詳細 |
| Relating first-order monadic omega-logic, propositional linear-time temporal logic, propositional generalized definitional reflection logic and propositional infinitary logic | Journal of Logic and Computation 27 (7), pp. 2271-2301, Oxford University Press, 2017. | 上出哲広 研究室 | 詳細 |
| Paraconsistent sequential linear-time temporal logic: Combining paraconsistency and sequentiality in temporal reasoning | Reports on Mathematical Logic 52, pp. 3-44, Jagiellonian University Press, 2017. | 上出哲広 研究室 | 詳細 |
| Paraconsistent double negations as classical and intuitionistic negations | Studia Logica 105 (6), pp. 1167-1191, Springer, 2017. | 上出哲広 研究室 | 詳細 |
| Kripke Completeness of bi-intuitionistic multilattice logic and its connexive variant | Studia Logica 105 (6), pp. 1193-1219, Springer, 2017. | 上出哲広 研究室 | 詳細 |
| Decidable temporal and sequential relevant logics | Journal of Logic and Computation, Online first, Oxford University Press, 2017. | 上出哲広 研究室 | 詳細 |
| Paraconsistent sequential linear-time temporal logic and its application to clinical reasoning verification: A brief survey and future work | International Journal of Applied & Experimental Mathematics 2 (2), IJAEM-121, 2 pages, Graphy Publications, 2017. | 上出哲広 研究室 | 詳細 |
| Logics and translations for inconsistency-tolerant model checking | Proceedings of the 10th International Conference on Agents and Artificial Intelligence (ICAART 2018), Vol. 2, pp. 191-200, Science and Technology Publications, 2018. | 上出哲広 研究室 | 詳細 |
| 題名 | 研究室 | 内容 |
|---|---|---|
| Bunched sequential information | 上出哲広研究室 | 詳細 |
| A decidable paraconsistent relevant logic: Gentzen system and Routley-Meyer semantics | 上出哲広研究室 | 詳細 |
| Method for combining paraconsistency and sequentiality in temporal reasoning | 上出哲広研究室 | 詳細 |
| Completeness of connexive Heyting-Brouwer logic | 上出哲広研究室 | 詳細 |
| Paraconsistent double negation as a modal operator | 上出哲広研究室 | 詳細 |
| Cut-free systems for restricted bi-intuitionistic logic and its connexive extension | 上出哲広研究室 | 詳細 |
| Paraconsistent double negation that can simulate classical negation | 上出哲広研究室 | 詳細 |
| Intuitionistic De Morgan verification and falsification logics | 上出哲広研究室 | 詳細 |
| Duality in some intuitionistic paraconsistent logics | 上出哲広研究室 | 詳細 |
| Logics with definitional reflection rules | 上出哲広研究室 | 詳細 |
| Embedding from multilattice logic into classical logic and vice versa | 上出哲広研究室 | 詳細 |
| Relating first-order monadic omega-logic, propositional linear-time temporal logic, propositional generalized definitional reflection logic and propositional infinitary logic | 上出哲広研究室 | 詳細 |
| Proof theory of paraconsistent quantum logic | 上出哲広研究室 | 詳細 |
学会発表
| 演題名 | 学会名 | 研究室 | 内容 |
|---|---|---|---|
| Notes on Avron's self-extensional four-valued paradefinite logic | The 51st IEEE International Symposium on Multiple-Valued Logic | 上出哲広 研究室 | 詳細 |
| Symmetric Paraconsistent Quantum Logic | The 51st IEEE International Symposium on Multiple-Valued Logic | 上出哲広 研究室 | 詳細 |
| Expanding the realm of Belnap-Dunn logic: Self-extensional four-valued paradefinite logic, subtrilattice logic, and symmetric paraconsistent quantum logic | Colloquium on Loigc and Epistemology in Bochum | 上出哲広研究室 | 詳細 |
| Reasoning with inconsistency-tolerant fuzzy description logics | The 14th International Conference on Agents and Artificial Intelligence (ICAART 2022) | 上出哲広研究室 | 詳細 |
| Falsification-aware semantics for CTL and its inconsistency-tolerant subsystem: Towards falsification-aware model checking | The 14th International Conference on Agents and Artificial Intelligence (ICAART 2022) | 上出哲広研究室 | 詳細 |
| Inconsistency-tolerant hierarchical probabilistic computation tree logic model checking and its application to clinical reasoning verification | The 7th International Conference on Fuzzy Systems and Data Mining (FSDM 2021) | 上出哲広研究室 | 詳細 |
| 反証的CTLモデル検査の拡張とその応⽤ | 情報処理学会第84回全国⼤会 | 上出哲広研究室 | 詳細 |
| 演題名 | 学会名 | 研究室 | 内容 |
|---|---|---|---|
| Inconsistency-tolerant fuzzy description logics | The 6th International Conference on Fuzzy Systems and Data Mining (FSDM 2020) | 上出哲広 研究室 | 詳細 |
| Sequential fuzzy description logic: Reasoning for fuzzy knowledge bases with sequential information | The 50th IEEE International Symposium on Multiple-Valued Logic (ISMVL 2020) | 上出哲広 研究室 | 詳細 |
| Completeness of subtrilattice logic | The 50th IEEE International Symposium on Multiple-Valued Logic (ISMVL 2020) | 上出哲広 研究室 | 詳細 |
| Inconsistency-tolerant hierarchical probabilistic computation tree logic and its application to model checking | The 13th International Conference on Agents and Artificial Intelligence (ICAART 2021) | 上出哲広 研究室 | 詳細 |
| ⽭盾許容階層確率モデル検査技術を⽤いた臨床推論・知識検証技法の提案 | 情報処理学会, 研究報告数理モデル化と問題解決(MPS) | 上出哲広 研究室 | 詳細 |
| ⽭盾許容階層確率CTLモデル検査に対する論理と具体例 | 情報処理学会第83回全国⼤会 | 上出哲広 研究室 | 詳細 |
| 演題名 | 学会名 | 研究室 | 内容 |
|---|---|---|---|
| Finite model property for modal ideal paraconsistent four-valued logic | The 49th IEEE International Symposium on Multiple-Valued Logic (ISMVL 2019) | 上出哲広 研究室 | 詳細 |
| First-order Nelsonian paraconsistent quantum logic | The 49th IEEE International Symposium on Multiple-Valued Logic (ISMVL 2019) | 上出哲広 研究室 | 詳細 |
| 矛盾許容階層確率CTLモデル検査とその臨床推論検証への応用 | 日本ソフトウェア科学会第36回大会 | 上出哲広 研究室 | 詳細 |
| 【学術会議招待講演】Logical foundation of locative inconsistency-tolerant hierarchical probabilistic model checking | The 5th International Conference on Fuzzy Systems and Data Mining (FSDM 2019) | 上出哲広 研究室 | 詳細 |
| 【学術会議招待講演】Extending Probabilistic Model Checking | The 3rd International Conference on Software and e-Business (ICSEB 2019) | 上出哲広 研究室 | 詳細 |
| An extended description logic for inconsistency-tolerant ontological reasoning with sequential information | The 12th International Conference on Agents and Artificial Intelligence (ICAART 2020) | 上出哲広 研究室 | 詳細 |
| 演題名 | 学会名 | 研究室 | 内容 |
|---|---|---|---|
| ソフトシステム方法論に基づく教育・学習支援ツールの開発 | 日本ソフトウェア科学会 | 上出哲広研究室 | 詳細 |
| ソフトシステム方法論を用いた教育カリキュラム設計における概念モデルの形式検証 | 日本ソフトウェア科学会 | 上出哲広研究室 | 詳細 |
| Foundations of Hierarchical Model Checking: Logics, Translations, and Examples | The 4th International Conference on Fuzzy Systems and Data Mining | 上出哲広研究室 | 詳細 |
| An extended paradefinte Belnap-Dunn logic that is embeddable into classical logic and vice versa | The 11th International Conference on Agents and Artificial Intelligence | 上出哲広研究室 | 詳細 |
| Towards hierarchical probabilistic CTL model checking: Theoretical foundations | The 11th International Conference on Agents and Artificial Intelligence | 上出哲広研究室 | 詳細 |
| Towards locative inconsistency-tolerant hierarchical probabilistic CTL model checking: Survey and future work | The 11th International Conference on Agents and Artificial Intelligence | 上出哲広研究室 | 詳細 |
| 演題名 | 学会名 | 研究室 | 内容 |
|---|---|---|---|
| Phase semantics for multilattice formalism, | The 47th IEEE International Symposium on Multiple-Valued Logic (ISMVL 2017) | 上出哲広研究室 | 詳細 |
| Extending ideal paraconsistent four-valued logic | The 47th IEEE International Symposium on Multiple-Valued Logic (ISMVL 2017) | 上出哲広研究室 | 詳細 |
| Natural deduction for connexive paraconsistent quantum logic | The 47th IEEE International Symposium on Multiple-Valued Logic (ISMVL 2017) | 上出哲広研究室 | 詳細 |
| An extended first-order Belnap-Dunn logic with classical negation | The 6th International Workshop on Logic, Rationality, and Interaction (LORI 2017) | 上出哲広研究室 | 詳細 |
| Bi-classical connexive logic and its modal extension: Cut-elimination, completeness and duality | The 3rd Workshop on connexive logics | 上出哲広研究室 | 詳細 |
| 矛盾許容モデル検査のための論理と翻訳 | 日本ソフトウェア科学会 | 上出哲広研究室 | 詳細 |
| 矛盾許容モデル検査の臨床推論検証および学習プロセス検証への応用 | 日本ソフトウェア科学会 | 上出哲広研究室 | 詳細 |
| 階層モデル検査による階層的推論プロセスの検証 | 日本ソフトウェア科学会 | 上出哲広研究室 | 詳細 |
| 階層モデル検査： 論理, 翻訳および具体例 | 情報処理学会 数理モデル化と問題解決研究会 | 上出哲広研究室 | 詳細 |
| Paraconsistent model checking: Logics, translations and examples | 2017 International Conference on Software and e-Business (ICSEB 2017), Hong Kong, 28-30 December, 2017. | 上出哲広研究室 | 詳細 |
| Logics and translations for inconsistency-tolerant model checking | The 10th International Conference on Agents and Artificial Intelligence (ICAART 2018), Funchal, Madeira – Portugal, 16-18 January, 2018. | 上出哲広研究室 | 詳細 |
| 演題名 | 学会名 | 研究室 | 内容 |
|---|---|---|---|
| Paraconsistent sequential linear-time temporal logic and its application to medical reasoning | 科学基礎論学会2016年度研究例会ワークショップ | 上出哲広研究室 | 詳細 |
| Paraconsistent double negation that can simulate classical negation | The 46th IEEE International Symposium on Multiple-Valued Logic (ISMVL 2016) | 上出哲広研究室 | 詳細 |
| Cut-free systems for restricted bi-intuitionistic logic and its connexive extension | The 46th IEEE International Symposium on Multiple-Valued Logic (ISMVL 2016) | 上出哲広研究室 | 詳細 |
先生ってこんな人研究の詳細や、研究に対する熱い思いなどを更に詳しくご紹介します
先生方が日々取り組んでいる研究について、どのようなきっかけで取り組むようになったのか、その研究はどのような形で社会に生かされていくのかなど、研究室紹介だけでは紹介しきれない内容や、普段なかなか知ることのできない先生方の研究に対する熱い思いなどをご紹介します。