• 研究課題をさがす
  • 研究者をさがす
  • KAKENの使い方
  1. 前のページに戻る

条件付き項書き換えシステムにおける帰納的定理と基底合流性に関する研究

研究課題

研究課題/領域番号 18K11158
研究種目

基盤研究(C)

配分区分基金
応募区分一般
審査区分 小区分60010:情報学基礎論関連
研究機関新潟大学

研究代表者

青戸 等人  新潟大学, 自然科学系, 教授 (00293390)

研究期間 (年度) 2018-04-01 – 2022-03-31
研究課題ステータス 完了 (2021年度)
配分額 *注記
4,420千円 (直接経費: 3,400千円、間接経費: 1,020千円)
2020年度: 1,430千円 (直接経費: 1,100千円、間接経費: 330千円)
2019年度: 1,430千円 (直接経費: 1,100千円、間接経費: 330千円)
2018年度: 1,560千円 (直接経費: 1,200千円、間接経費: 360千円)
キーワード帰納的定理 / 基底合流性 / 条件付き項書き換えシステム / ホーン節論理 / 合流性 / 項書き換えシステム / ホーン節帰納的定理 / 補題生成法 / アンラベリング変換 / 定理自動証明
研究成果の概要

項書き換えシステムは,形式手法に基づくソフトウェア構成・検証技術の基礎を与える重要な計算モデルである. 帰納的定理は,項書き換えシステムをプログラムとして見做したときに成立する性質に対応し,基底合流性は,項書き換えシステムの解析において重要な解の一意性を保証する性質である. 条件付き項書き換えシステムは,ホーン節論理の書き換えシステムによるモデル化であり,関数型プログラムのモデルとして,応用上重要な拡張である.本研究では,指向式条件付き項書き換えシステムにおけるホーン節帰納的定理証明のための書き換え帰納法,指向式条件付き項書き換えシステムの基底合流性検証法,階層可換性の十分条件などを与えた.

研究成果の学術的意義や社会的意義

項書き換えシステムは,論理的な推論体系と計算手続きを表わす計算体系と2面性を持つ計算モデルであり,合流性や帰納的な妥当性はその両方の側面を繋ぐ重要な性質と考えることができる.本研究は,安全なソフトウェアを構築するための基礎理論に関するものであり,長期的には情報システムの脆弱性の克服への貢献となるものと考えられる.

報告書

(5件)
  • 2021 実績報告書   研究成果報告書 ( PDF )
  • 2020 実施状況報告書
  • 2019 実施状況報告書
  • 2018 実施状況報告書
  • 研究成果

    (22件)

すべて 2021 2020 2019 2018

すべて 雑誌論文 (15件) (うち国際共著 2件、 査読あり 15件、 オープンアクセス 6件) 学会発表 (7件)

  • [雑誌論文] 圏論に基づく正則項上の単一化の形式化2021

    • 著者名/発表者名
      宮前 海里, 青戸 等人
    • 雑誌名

      情報処理学会論文誌プログラミング(PRO)

      巻: 14 ページ: 1-14

    • NAID

      170000184922

    • 関連する報告書
      2021 実績報告書
    • 査読あり
  • [雑誌論文] フラット項書き換えシステムにおける正規形の一意性に関する性質の決定不能性2021

    • 著者名/発表者名
      佐藤 悠稀 , 青戸 等人
    • 雑誌名

      情報処理学会論文誌プログラミング(PRO)

      巻: 14 ページ: 15-24

    • NAID

      170000184921

    • 関連する報告書
      2021 実績報告書
    • 査読あり
  • [雑誌論文] Commutative rational term rewriting2021

    • 著者名/発表者名
      Mamoru Ishizuka, Takahito Aoto and Munehiro Iwami
    • 雑誌名

      Proceedings of the 15th International Conference on Language and Automata Theory and Applications (LATA 2021), Lecture Notes in Computer Science,

      巻: 12638 ページ: 200-212

    • DOI

      10.1007/978-3-030-68195-1_15

    • ISBN
      9783030681944, 9783030681951
    • 関連する報告書
      2020 実施状況報告書
    • 査読あり
  • [雑誌論文] 対話的定理証明器Isabelle/HOL上での書き換え帰納法の形式化2020

    • 著者名/発表者名
      木村 優太, 青戸 等人
    • 雑誌名

      コンピュータ ソフトウェア

      巻: 37 号: 2 ページ: 2_104-2_119

    • DOI

      10.11309/jssst.37.2_104

    • NAID

      130007844692

    • ISSN
      0289-6540
    • 年月日
      2020-04-23
    • 関連する報告書
      2020 実施状況報告書
    • 査読あり / オープンアクセス
  • [雑誌論文] A fast decision procedure for uniqueness of normal forms w.r.t. conversion of shallow term rewriting systems2020

    • 著者名/発表者名
      Masaomi Yamaguchi and Takahito Aoto
    • 雑誌名

      Proceedings of the 5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020), Leibniz International Proceedings in Informatics,

      巻: 167

    • 関連する報告書
      2020 実施状況報告書
    • 査読あり / オープンアクセス
  • [雑誌論文] 項書き換えシステムにおける局所十分完全性の証明法2020

    • 著者名/発表者名
      白石智輝, 青戸等人, 菊池健太郎
    • 雑誌名

      第22回プログラミングおよびプログラミング言語ワークショップ(PPL 2020)論文集

      巻: C1-12 ページ: 1-15

    • 関連する報告書
      2019 実施状況報告書
    • 査読あり
  • [雑誌論文] 条件付き項書き換えシステムの階層合流性証明法2020

    • 著者名/発表者名
      加賀谷有輝, 青戸等人
    • 雑誌名

      第22回プログラミングおよびプログラミング言語ワークショップ(PPL 2020)論文集

      巻: C1-14 ページ: 1-12

    • NAID

      170000180844

    • 関連する報告書
      2019 実施状況報告書
    • 査読あり
  • [雑誌論文] 交換律による正則項書き換えにおける有限オートマトンの構成法とその応用2020

    • 著者名/発表者名
      石塚守, 青戸等人, 岩見宗弘
    • 雑誌名

      第22回プログラミングおよびプログラミング言語ワークショップ(PPL 2020)論文集

      巻: C1-17 ページ: 1-12

    • 関連する報告書
      2019 実施状況報告書
    • 査読あり
  • [雑誌論文] 条件付き項書き換えシステムにおけるホーン節帰納的定理の自動証明2019

    • 著者名/発表者名
      栗田 泰智, 青戸 等人
    • 雑誌名

      コンピュータ ソフトウェア

      巻: 36 号: 2 ページ: 2_61-2_75

    • DOI

      10.11309/jssst.36.2_61

    • NAID

      130007666999

    • ISSN
      0289-6540
    • 年月日
      2019-04-26
    • 関連する報告書
      2019 実施状況報告書
    • 査読あり / オープンアクセス
  • [雑誌論文] Automated proofs of unique normal forms w.r.t. conversion for term rewriting systems2019

    • 著者名/発表者名
      Takahito Aoto and Yoshihito Toyama
    • 雑誌名

      Proceedings of the 12th International Symposium on Frontiers of Combining Systems (FroCoS 2019), LNCS

      巻: 11715 ページ: 330-347

    • DOI

      10.1007/978-3-030-29007-8_19

    • ISBN
      9783030290061, 9783030290078
    • 関連する報告書
      2019 実施状況報告書
    • 査読あり
  • [雑誌論文] Inductive Theorem Proving in Non-terminating Rewriting Systems and Its Application to Program Transformation2019

    • 著者名/発表者名
      Kentaro Kikuchi, Takahito Aoto, Isao Sasano
    • 雑誌名

      Proceedings of the 21st International Symposium on Principles and Practice of Declarative Programming (PPDP 2019)

      巻: 21 ページ: 1-14

    • DOI

      10.1145/3354166.3354178

    • 関連する報告書
      2019 実施状況報告書
    • 査読あり / オープンアクセス / 国際共著
  • [雑誌論文] 条件付き項書き換えシステムにおけるホーン節帰納的定理の自動証明2019

    • 著者名/発表者名
      栗田泰智, 青戸等人
    • 雑誌名

      コンピュータソフトウェア

      巻: 36 ページ: 61-75

    • NAID

      130007666999

    • 関連する報告書
      2018 実施状況報告書
    • 査読あり / オープンアクセス
  • [雑誌論文] 書き換え帰納法を利用した帰納的定理証明の補題生成法2019

    • 著者名/発表者名
      加藤裕人, 青戸等人
    • 雑誌名

      第21回プログラミングおよびプログラミング言語ワークショップ

      巻: 21 ページ: 1-15

    • NAID

      40021462142

    • 関連する報告書
      2018 実施状況報告書
    • 査読あり
  • [雑誌論文] 決定手続きを用いた項書き換えシステムの帰納的定理自動証明2019

    • 著者名/発表者名
      山口諒, 青戸等人
    • 雑誌名

      第21回プログラミングおよびプログラミング言語ワークショップ

      巻: 21 ページ: 1-14

    • NAID

      40022502359

    • 関連する報告書
      2018 実施状況報告書
    • 査読あり
  • [雑誌論文] Confluence Competition 20182018

    • 著者名/発表者名
      T. Aoto, M. Hamana, N. Hirokawa, A. Middeldorp J. Nagele, N. Nishida, K. Shintani, and Harald Zankl
    • 雑誌名

      Leibniz International Proceedings in Informatics (LIPIcs)

      巻: 108

    • DOI

      10.4230/LIPIcs.FSCD.2018.32

    • NAID

      120006705615

    • 関連する報告書
      2018 実施状況報告書
    • 査読あり / オープンアクセス / 国際共著
  • [学会発表] 圏論にもとづく正則項上の単一化の形式化2020

    • 著者名/発表者名
      宮前海里, 青戸等人
    • 学会等名
      第131回プログラミング研究発表会
    • 関連する報告書
      2020 実施状況報告書
  • [学会発表] 外部変数のある可換式条件付き項書き換えシステムの合流性条件2020

    • 著者名/発表者名
      笹川葵生, 青戸等人
    • 学会等名
      第131回プログラミング研究発表会
    • 関連する報告書
      2020 実施状況報告書
  • [学会発表] フラット項書き換えシステムにおける正規形の一意性に関する性質の決定不能性2020

    • 著者名/発表者名
      佐藤悠稀, 青戸等人
    • 学会等名
      第131回プログラミング研究発表会
    • 関連する報告書
      2020 実施状況報告書
  • [学会発表] Proving sufficient completeness w.r.t. reduction of CTRSs automatically2020

    • 著者名/発表者名
      Takahito Aoto
    • 学会等名
      第52回 TRS ミーティング
    • 関連する報告書
      2019 実施状況報告書
  • [学会発表] Level-confluence of left-linear overlapping CTRSs2019

    • 著者名/発表者名
      Takahito Aoto
    • 学会等名
      第51回 TRS ミーティング
    • 関連する報告書
      2019 実施状況報告書
  • [学会発表] Jaffarのアルゴリズムに基づく正則項の単一化2018

    • 著者名/発表者名
      石塚守, 青戸等人
    • 学会等名
      日本ソフトウェア科学会第35回大会
    • 関連する報告書
      2018 実施状況報告書
  • [学会発表] 決定手続きを用いた項書き換えシステムの帰納的定理自動証明2018

    • 著者名/発表者名
      山口諒, 青戸等人
    • 学会等名
      日本ソフトウェア科学会第35回大会
    • 関連する報告書
      2018 実施状況報告書

URL: 

公開日: 2018-04-23   更新日: 2023-03-16  

サービス概要 検索マニュアル よくある質問 お知らせ 利用規程 科研費による研究の帰属

Powered by NII kakenhi