研究者詳細

顔写真

オダ　ユキヒロ
織田　幸弘
Yukihiro Oda
所属
大学院情報科学研究科　情報基礎科学専攻　ソフトウェア科学講座（ソフトウェア基礎科学分野）
職名
特任研究員
学位

  • 博士（情報学） （総合研究大学院大学）

プロフィール

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

経歴 1

  • 2023年4月 ～ 継続中
    東北大学　大学院情報科学研究科　特任研究員

学歴 2

  • 総合研究大学院大学　複合科学研究科　情報学専攻

    2018年4月 ～ 2024年3月

  • 慶應義塾大学　理工学部　数理科学科

    2010年4月 ～ 2015年9月

研究キーワード 3

  • 数理論理学

  • 循環証明体系

  • 論理学

研究分野 2

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

  • 自然科学一般 / 数学基礎 / 数理論理学

論文 6

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

    Yukihiro Oda, Eijiro Sumii

    CoRR　abs/2606.27059　2026年6月

    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年4月

    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年2月

    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年3月11日

    詳細を見る 詳細を閉じる

    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.

︎全件表示 ︎最初の5件までを表示

共同研究・競争的資金等の研究課題 1

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

    織田 幸弘

    2026年4月1日 ～ 2031年3月31日