Details of the Researcher

PHOTO

Yukihiro Oda
Section
Graduate School of Information Sciences
Job title
Specially Appointed Research Fellow
Degree

  • Doctor of Philosophy (The Graduate University for Advanced Studies)

Profile

論理に関わること全般に興味をもっています．循環証明体系の証明論的な性質を主に研究しています．

Research History 1

  • 2023/04 - Present
    Tohoku University　Graduate School of Information Sciences　Specially Appointed Research Fellow

Education 2

  • The Graduate University for Advanced Studies　School of Multidisciplinary Sciences　Department of Informatics

    2018/04 - 2024/03

  • Keio University　Faculty of Science and Technology　Department of Mathematics

    2010/04 - 2015/09

Research Interests 3

  • Mathematical Logic

  • Cyclic proofs/cicular proofs

  • Logic

Research Areas 2

  • Informatics / Information theory /

  • Natural sciences / Basic mathematics / Mathematical Logic

Papers 6

  1. Type-based information flow analysis for π-calculus with a dynamically extensible security lattice.

    Yukihiro Oda, Eijiro Sumii

    CoRR　abs/2606.27059　2026/06

    DOI： 10.48550/arXiv.2606.27059 　

  2. A study of cut-elimination for a non-labelled cyclic proof system for propositional dynamic logics.

    Yukihiro Oda

    CoRR　abs/2512.15075　2025/12

    DOI： 10.48550/arXiv.2512.15075 　

  3. Cyclic Proofs in Hoare Logic and its Reverse.

    James Brotherston, Quang Loc Le, Gauri Desai, Yukihiro Oda

    MFPS　2025/04

    DOI： 10.46298/entics.16696 　 10.48550/arXiv.2504.14283 　

  4. Proof systems for partial incorrectness logic (partial reverse Hoare logic).

    Yukihiro Oda

    CoRR　abs/2502.21053　2025/02

    DOI： 10.48550/arXiv.2502.21053 　

  5. The failure of cut-elimination in cyclic proof for first-order logic with inductive definitions.

    Yukihiro Oda, James Brotherston, Makoto Tatsuta

    J. Log. Comput.　35　(2)　2025

    DOI： 10.1093/logcom/exad068 　

  6. A study for recovering the cut-elimination property in cyclic proof systems by restricting the arity of inductive predicates

    Yukihiro Oda, Daisuke Kimura

    2022/03/11

    More details Close

    The framework of cyclic proof systems provides a reasonable proof system for logics with inductive definitions. It also offers an effective automated proof search procedure for such logics without finding induction hypotheses. Recent researches have shown that the cut-elimination property, one of the most fundamental properties in proof theory, of cyclic proof systems for several logics does not hold. These results suggest that a naive proof search, which avoids the Cut rule, is not enough. This paper shows that the cut-elimination property still fails in a simple cyclic proof system even if we restrict languages to unary inductive predicates and unary functions, aiming to clarify why the cut-elimination property fails in the cyclic proof systems. The result in this paper is a sharper one than that of the first authors' previous result, which gave a counterexample using two ternary inductive predicates and a unary function symbol to show the failure of the cut-elimination property in the cyclic proof system of the first-order logic.

Show all ︎Show first 5

Research Projects 1

  1. 非整礎証明体系，特に循環証明体系の証明論

    織田 幸弘

    Offer Organization: 日本学術振興会

    System: 科学研究費助成事業

    Category: 若手研究

    Institution: 東北大学

    2026/04/01 - 2031/03/31