研究者詳細

顔写真

サオトメ　ケンジ
早乙女　献自
Kenji Saotome
所属
電気通信研究所　計算システム基盤研究部門　ソフトウエア構成研究室
職名
特任研究員
学位

  • 博士（情報学） （名古屋大学）

経歴 2

  • 2026年4月 ～ 継続中
    東北大学　電気通信研究所　特任研究員

  • 2021年4月 ～ 2025年3月
    SECOM株式会社 IS研究所　サービスエンジニアリングディビジョン　研究員

学歴 2

  • 名古屋大学　大学院情報学研究科　情報システム学専攻

    2023年4月 ～ 2026年3月

  • 名古屋大学　大学院情報学研究科　情報システム学専攻

    2019年4月 ～ 2021年3月

研究キーワード 3

  • 形式検証

  • 数理論理学

  • 循環証明体系

研究分野 2

  • 情報通信 / ソフトウェア /

  • 情報通信 / 情報学基礎論 / 数理論理学

受賞 2

  1. エクセレントドクター賞

    2026年3月　名古屋大学大学院情報学研究科

  2. 山下記念研究賞

    2025年　情報処理学会

論文 5

  1. Failure of cut-elimination in cyclic-proof systems of logic of bunched implications with inductive propositions 査読有り

    Kenji Saotome, Koji Nakazawa, Daisuke Kimura, Ayumu Kawasaki

    Archive for Mathematical Logic　65　(3)　333-362　2025年11月21日

    出版者・発行元： Springer Science and Business Media LLC

    DOI： 10.1007/s00153-025-00993-2 　

    ISSN：0933-5846

    eISSN：1432-0665

    詳細を見る 詳細を閉じる

    Abstract Cyclic-proof systems are sequent-calculus-style proof systems that allow circular structures that represent induction. Cyclic-proof systems are considered suitable for automated inductive reasoning, and the cut-elimination property is desirable because finding cut formulas often requires heuristics. However, the cut-elimination property does not hold in some cyclic-proof systems, such as the sequent calculus for first-order logic and the entailment system for symbolic-heap separation logic. This paper proves that the cyclic-proof system for the logic of bunched implications does not satisfy the cut-elimination property, even if the system is restricted to the positive fragment with inductively defined propositions. To prove this, we use a new proof technique called proof unrolling. To demonstrate that proof unrolling is a general technique, this paper adapts proof unrolling to another cyclic-proof system for multiplicative additive linear logic with fixed-point operators.

  2. Cyclic-proof Systems for Symbolic Heaps Require Cut Formulas Outside Initial Signatures 査読有り

    Kenji Saotome, Koji Nakazawa

    Journal of Information Processing　33　445-460　2025年

    出版者・発行元： Information Processing Society of Japan

    DOI： 10.2197/ipsjjip.33.445 　

    eISSN：1882-6652

  3. Restriction on cut rule in cyclic-proof system for symbolic heaps 査読有り

    早乙女献自, 中澤巧爾, 木村大輔

    Theoretical Computer Science　1019　114854-114854　2024年12月

    出版者・発行元：

    DOI： 10.1016/j.tcs.2024.114854 　

    ISSN：0304-3975

  4. Failure of cut-elimination in the cyclic proof system of bunched logic with inductive propositions 査読有り

    Kenji Saotome, Koji Nakazawa, Daisuke Kimura

    Leibniz International Proceedings in Informatics, LIPIcs　195　2021年7月1日

    出版者・発行元： Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing

    DOI： 10.4230/LIPIcs.FSCD.2021.11 　

    ISSN：1868-8969

  5. Restriction on Cut in Cyclic Proof System for Symbolic Heaps

    Kenji Saotome, Koji Nakazawa, Daisuke Kimura

    Lecture Notes in Computer Science　88-105　2020年9月2日

    出版者・発行元： Springer International Publishing

    DOI： 10.1007/978-3-030-59025-3_6 　

    ISSN：0302-9743

    eISSN：1611-3349