Details of the Researcher

PHOTO

Kenji Saotome
Section
Research Institute of Electrical Communication
Job title
Specially Appointed Research Fellow
Degree

  • Doctor of Informatics (Nagoya University)

Research History 2

  • 2026/04 - Present
    Tohoku University　Research Institute of Electrical Communication　Specially Appointed Research Fellow

  • 2021/04 - 2025/03
    SECOM Intelligent Systems Laboratory　Service engineering division　Researcher

Education 2

  • Nagoya University　Graduate School of Informatics　Department of Computing and Software Systems

    2023/04 - 2026/03

  • Nagoya University　Graduate School of Informatics　Department of Computing and Software Systems

    2019/04 - 2021/03

Research Interests 3

  • formal verification

  • mathematical logic

  • cyclic proofs

Research Areas 2

  • Informatics / Software /

  • Informatics / Information theory / mathematical logic

Awards 2

  1. Excellent Doctor Award

    2026/03　Graduate School of Informatics, Nagoya University

  2. IPSJ Yamashita SIG Research Award

    2025　Information Processing Society of Japan　Cyclic-proof systems for symbolic heaps require cut formulas outside initial signatures

Papers 5

  1. Failure of cut-elimination in cyclic-proof systems of logic of bunched implications with inductive propositions Peer-reviewed

    Kenji Saotome, Koji Nakazawa, Daisuke Kimura, Ayumu Kawasaki

    Archive for Mathematical Logic　65　(3)　333-362　2025/11/21

    Publisher: Springer Science and Business Media LLC

    DOI： 10.1007/s00153-025-00993-2 　

    ISSN： 0933-5846

    eISSN： 1432-0665

    More details Close

    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 Peer-reviewed

    Kenji Saotome, Koji Nakazawa

    Journal of Information Processing　33　445-460　2025

    Publisher: 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 Peer-reviewed

    Kenji Saotome, Koji Nakazawa, Daisuke Kimura

    Theoretical Computer Science　1019　114854-114854　2024/12

    Publisher: Elsevier BV

    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 Peer-reviewed

    Kenji Saotome, Koji Nakazawa, Daisuke Kimura

    Leibniz International Proceedings in Informatics, LIPIcs　195　2021/07/01

    Publisher: 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/09/02

    Publisher: Springer International Publishing

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

    ISSN： 0302-9743

    eISSN： 1611-3349