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

定理自動証明における補題発見法に関する研究

研究課題

研究課題/領域番号 23500002
研究種目

基盤研究(C)

配分区分基金
応募区分一般
研究分野 情報学基礎
研究機関東北大学

研究代表者

青戸 等人  東北大学, 電気通信研究所, 准教授 (00293390)

研究分担者 外山 芳人  東北大学, 電気通信研究所, 教授 (00251968)
研究期間 (年度) 2011 – 2013
研究課題ステータス 完了 (2013年度)
配分額 *注記
5,070千円 (直接経費: 3,900千円、間接経費: 1,170千円)
2013年度: 1,300千円 (直接経費: 1,000千円、間接経費: 300千円)
2012年度: 2,340千円 (直接経費: 1,800千円、間接経費: 540千円)
2011年度: 1,430千円 (直接経費: 1,100千円、間接経費: 330千円)
キーワード項書き換えシステム / 自動定理証明 / 帰納的定理 / 補題発見
研究概要

書き換えシステムに基づく帰納的定理の自動証明における補題生成法について、補題候補の発見法や補題決定に有効な技術に資する成果を得た。主な研究成果としては、発散を生じる等式を解析するための基礎理論として、正則項の単一化および書き換え理論、半単一化についての理論について新しい知見を与えた。補題の決定手続きに適した書き換え帰納法の決定理論を拡張するとともに、書き換え帰納法において有効な補題決定手続きについて、始代数を用いるアプローチに基づく新しい手続きを考案した。また、書き換えシステムにおける末尾再帰を用いた関数定義において、自動証明に適した関数定義を得るための補題を抽出する手法を考案した。

報告書

(4件)
  • 2013 実績報告書   研究成果報告書 ( PDF )
  • 2012 実施状況報告書
  • 2011 実施状況報告書
  • 研究成果

    (42件)

すべて 2014 2013 2012 2011 その他

すべて 雑誌論文 (18件) (うち査読あり 18件) 学会発表 (22件) 備考 (2件)

  • [雑誌論文] ボトムアップ最内項書き換えシステムの最内到達可能性2014

    • 著者名/発表者名
      高橋翔大, 青戸等人, 外山芳人
    • 雑誌名

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

      巻: 31 号: 1 ページ: 1_75-1_89

    • DOI

      10.11309/jssst.31.1_75

    • NAID

      130004549336

    • ISSN
      0289-6540
    • 関連する報告書
      2013 実績報告書
    • 査読あり
  • [雑誌論文] Disproving confluence of term rewriting systems by interpretation and ordering, In Proceedings of the 9th International Symposium on Frontiers of Combining Systems (FroCoS 2013)2013

    • 著者名/発表者名
      Takahito Aoto
    • 雑誌名

      Lecture Notes in Artificial Intelligence

      巻: Vol.8152 ページ: 311-326

    • URL

      http://link.springer.com/chapter/10.1007%2F978-3-642-40885-4_22

    • 関連する報告書
      2013 研究成果報告書
    • 査読あり
  • [雑誌論文] 永続性に基づく項書き換えシステムの合流性証明法2013

    • 著者名/発表者名
      鈴木翼, 青戸等人, 外山芳人
    • 雑誌名

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

      巻: Vol.30, No.3 ページ: 148-162

    • 関連する報告書
      2013 実績報告書 2013 研究成果報告書
    • 査読あり
  • [雑誌論文] Termination of rule-based calculi for uniform semi-unification, In Proceedings of the 7th International Conference on Language and Automata Theory and Applications (LATA 2013)2013

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

      Lecture Notes in Computer Science

      巻: Vol.7810 ページ: 56-67

    • URL

      http://link.springer.com/chapter/10.1007%2F978-3-642-37064-9_7

    • 関連する報告書
      2013 研究成果報告書
    • 査読あり
  • [雑誌論文] 片側減少ダイアグラム法による項書き換えシステムの可換性証明法2013

    • 著者名/発表者名
      的場正樹, 青戸等人, 外山芳人
    • 雑誌名

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

      巻: Vol.30, No.1 ページ: 187-202

    • NAID

      130004549310

    • 関連する報告書
      2013 研究成果報告書 2012 実施状況報告書
    • 査読あり
  • [雑誌論文] ボトムアップ書き換えに基づく最内書き換え到達可能性判定2013

    • 著者名/発表者名
      高橋翔大, 青戸等人, 外山芳人
    • 雑誌名

      第15回プログラミングおよびプログラミング言語ワークショップ論文集

    • 関連する報告書
      2013 研究成果報告書
    • 査読あり
  • [雑誌論文] 書き換え帰納法に基づく帰納的定理の決定可能性2013

    • 著者名/発表者名
      中嶋辰成, 青戸等人, 外山芳人
    • 雑誌名

      第15回プログラミングおよびプログラミング言語ワークショップ論文集

    • NAID

      130004688287

    • 関連する報告書
      2013 研究成果報告書
    • 査読あり
  • [雑誌論文] Rational term rewriting revisited : decidability and confluence, In Proceedings of the 6th International Conference on Graph Transformation (ICGT 2012)2012

    • 著者名/発表者名
      Takahito Aoto and Jeroen Ketema
    • 雑誌名

      Lecture Notes in Computer Science

      巻: Vol.7562 ページ: 172-186

    • URL

      http://link.springer.com/chapter/10.1007%2F978-3-642-33654-6_12

    • 関連する報告書
      2013 研究成果報告書
    • 査読あり
  • [雑誌論文] A reduction-preserving completion for proving confluence of non-terminating term rewriting systems2012

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

      Logical Methods in Computer Science

      巻: Vol.8, No.1:31 ページ: 1-29

    • URL

      http://www.lmcs-online.org/ojs/viewarticle.php?id=1099&layout=abstract

    • 関連する報告書
      2013 研究成果報告書
    • 査読あり
  • [雑誌論文] 無限項書き換えシステムにおける強頭部正規化可能性および一般生成性の自動反証2012

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

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

      巻: Vol.29, No.1 ページ: 211-239

    • NAID

      130004549258

    • 関連する報告書
      2013 研究成果報告書
    • 査読あり
  • [雑誌論文] 多項式サイズ正規形を保証する項書き換えシステムの経路順序2012

    • 著者名/発表者名
      磯部耕己, 青戸等人, 外山芳人
    • 雑誌名

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

      巻: Vol.29, No.1 ページ: 176-190

    • NAID

      130004549256

    • 関連する報告書
      2013 研究成果報告書
    • 査読あり
  • [雑誌論文] 片側減少ダイアグラム法による項書き換えシステムの可換性証明法2012

    • 著者名/発表者名
      的場正樹, 青戸等人, 外山芳人
    • 雑誌名

      第14回プログラミングおよびプログラミング言語ワークショップ論文集

      ページ: 168-182

    • NAID

      130004549310

    • 関連する報告書
      2013 研究成果報告書
    • 査読あり
  • [雑誌論文] 永続性にもとづく項書き換えシステムの合流性証明2012

    • 著者名/発表者名
      鈴木翼, 青戸等人, 外山芳人
    • 雑誌名

      第14回プログラミングおよびプログラミング言語ワークショップ論文集

      ページ: 153-167

    • NAID

      40020657296

    • 関連する報告書
      2013 研究成果報告書
    • 査読あり
  • [雑誌論文] 多項式サイズ正規形を保証する項書き換えシステムの経路順序2012

    • 著者名/発表者名
      磯部耕己, 青戸等人, 外山 芳人
    • 雑誌名

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

      巻: Vol.129-1 ページ: 176-176

    • NAID

      130004549256

    • 関連する報告書
      2011 実施状況報告書
    • 査読あり
  • [雑誌論文] Natural inductive theorems for higher-order rewriting, In Proceedings of the 22nd International Conference on Rewriting Techniques and Applications (RTA 2011)2011

    • 著者名/発表者名
      Takahito Aoto, Toshiyuki Yamada and Yuki Chiba
    • 雑誌名

      Leibniz International Proceedings in Informatics, Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik

      巻: Vol.10 ページ: 107-121

    • URL

      http://drops.dagstuhl.de/opus/volltexte/2011/3111/

    • 関連する報告書
      2013 研究成果報告書
    • 査読あり
  • [雑誌論文] Reduction-preserving completion for proving confluence of non-terminating term rewriting systems In Proceedings of the 22nd International Conference on Rewriting Techniques and Applications (RTA 2011)2011

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

      Leibniz International Proceedings in Informatics, Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik

      巻: Vol.10 ページ: 91-106

    • URL

      http://drops.dagstuhl.de/opus/volltexte/2011/3110/

    • 関連する報告書
      2013 研究成果報告書
    • 査読あり
  • [雑誌論文] 多項式サイズ正規形を保証する項書き換えシステムの経路順序2011

    • 著者名/発表者名
      磯部耕己, 青戸等人, 外山芳人
    • 雑誌名

      第13回プログラミングおよびプログラミング言語ワークショップ論文集

      ページ: 99-113

    • NAID

      130004549256

    • 関連する報告書
      2013 研究成果報告書
    • 査読あり
  • [雑誌論文] 基底項書き換え系の多項式時間合流性判定法の改良2011

    • 著者名/発表者名
      村井正勝, 青戸等人, 外山芳人
    • 雑誌名

      第13回プログラミングおよびプログラミング言語ワークショップ論文集

      ページ: 84-98

    • 関連する報告書
      2013 研究成果報告書
    • 査読あり
  • [学会発表] 帰納的定理自動証明のための項書き換えシステム自動変換2014

    • 著者名/発表者名
      佐藤洸一, 菊池健太郎, 青戸等人, 外山芳人
    • 学会等名
      第16回プログラミングおよびプログラミング言語ワークショップ
    • 発表場所
      阿蘇
    • 関連する報告書
      2013 実績報告書
  • [学会発表] 閉包操作に基づく右基底項書き換えシステムの到達可能性判定2014

    • 著者名/発表者名
      四方駿作, 青戸等人, 外山芳人
    • 学会等名
      第16回プログラミングおよびプログラミング言語ワークショップ
    • 発表場所
      阿蘇
    • 関連する報告書
      2013 実績報告書
  • [学会発表] 永続性と減少ダイアグラム法に基づく合流性自動証明2014

    • 著者名/発表者名
      内田和真, 青戸等人, 外山芳人
    • 学会等名
      第16回プログラミングおよびプログラミング言語ワークショップ
    • 発表場所
      阿蘇
    • 関連する報告書
      2013 実績報告書
  • [学会発表] 名目書き換えシステムの合流性について2014

    • 著者名/発表者名
      鈴木貴樹, 菊池健太郎, 青戸等人, 外山芳人
    • 学会等名
      第16回プログラミングおよびプログラミング言語ワークショップ
    • 発表場所
      阿蘇
    • 関連する報告書
      2013 実績報告書
  • [学会発表] 自動検証のためのプログラム変換2013

    • 著者名/発表者名
      佐藤洸一, 菊池健太郎, 青戸等人, 外山芳人
    • 学会等名
      日本ソフトウェア科学会第30回大会
    • 発表場所
      東京
    • 年月日
      2013-09-13
    • 関連する報告書
      2013 研究成果報告書
  • [学会発表] 閉包操作に基づく項書き換えシステムの到達可能性判定2013

    • 著者名/発表者名
      四方駿作, 青戸等人, 外山芳人
    • 学会等名
      日本ソフトウェア科学会第30回大会
    • 発表場所
      東京
    • 年月日
      2013-09-13
    • 関連する報告書
      2013 研究成果報告書
  • [学会発表] 永続性と減少ダイアグラム法に基づく合流性証明法2013

    • 著者名/発表者名
      内田和真, 青戸等人, 外山芳人
    • 学会等名
      日本ソフトウェア科学会第30回大会
    • 発表場所
      東京
    • 年月日
      2013-09-13
    • 関連する報告書
      2013 研究成果報告書
  • [学会発表] Disproving confluence of term rewriting systems by interpretation and ordering (extended abstract)2013

    • 著者名/発表者名
      Takahito Aoto
    • 学会等名
      Proceedings of the 2nd International Workshop on Confluence (IWC 2013)
    • 発表場所
      Eindhoven, The Netherlands
    • 年月日
      2013-06-28
    • 関連する報告書
      2013 研究成果報告書
  • [学会発表] Termination of rule-based calculi for uniform semi-unification2013

    • 著者名/発表者名
      Takahito Aoto and Munehiro Iwami
    • 学会等名
      the 7th International Conference on Language and Automata Theory and Applications
    • 発表場所
      Bilbao, Spain
    • 関連する報告書
      2013 実績報告書
  • [学会発表] Disproving confluence of term rewriting systems by interpretation and ordering2013

    • 著者名/発表者名
      Takahito Aoto
    • 学会等名
      the 9th International Symposium on Frontiers of Combining Systems
    • 発表場所
      Nancy, France
    • 関連する報告書
      2013 実績報告書
  • [学会発表] Disproving confluence of term rewriting systems by interpretation and ordering (extended abstract)2013

    • 著者名/発表者名
      Takahito Aoto
    • 学会等名
      the 2nd International Workshop on Confluence
    • 発表場所
      Eindhoven, The Netherlands
    • 関連する報告書
      2013 実績報告書
  • [学会発表] ボトムアップ書き換えに基づく最内書き換え到達可能性判定2013

    • 著者名/発表者名
      高橋翔大, 青戸等人, 外山芳人
    • 学会等名
      第15回プログラミングおよびプログラミング言語ワークショップ
    • 発表場所
      会津若松
    • 関連する報告書
      2012 実施状況報告書
  • [学会発表] 書き換え帰納法に基づく帰納的定理の決定可能性2013

    • 著者名/発表者名
      中嶋辰成, 青戸等人, 外山芳人
    • 学会等名
      第15回プログラミングおよびプログラミング言語ワークショップ
    • 発表場所
      会津若松
    • 関連する報告書
      2012 実施状況報告書
  • [学会発表] 木オートマトンに基づく項書き換えシステムの逆計算2012

    • 著者名/発表者名
      椛澤涼, 青戸等人, 外山芳人
    • 学会等名
      日本ソフトウェア科学会第29回大会
    • 発表場所
      東京
    • 年月日
      2012-08-22
    • 関連する報告書
      2013 研究成果報告書
  • [学会発表] ボトムアップ書き換えに基づく到達可能性の判定法2012

    • 著者名/発表者名
      高橋翔大, 青戸等人, 外山芳人
    • 学会等名
      日本ソフトウェア科学会第29回大会
    • 発表場所
      東京
    • 年月日
      2012-08-22
    • 関連する報告書
      2013 研究成果報告書
  • [学会発表] 書き換え帰納法に基づく帰納的定理の決定手続き2012

    • 著者名/発表者名
      中嶋辰成, 青戸等人, 外山芳人
    • 学会等名
      日本ソフトウェア科学会第29回大会
    • 発表場所
      東京
    • 年月日
      2012-08-22
    • 関連する報告書
      2013 研究成果報告書
  • [学会発表] Transformations by templates for simply-typed term rewriting2012

    • 著者名/発表者名
      Yuki Chiba and Takahito Aoto
    • 学会等名
      Proceedings of the 6th International Workshop on Higher-Order Rewriting (HOR 2012)
    • 発表場所
      Nagoya, Japan
    • 年月日
      2012-06-02
    • 関連する報告書
      2013 研究成果報告書
  • [学会発表] Transformations by templates for simply-typed term rewriting2012

    • 著者名/発表者名
      Yuki Chiba and Takahito Aoto
    • 学会等名
      6th International Workshop on Higher-Order Rewriting
    • 発表場所
      名古屋
    • 関連する報告書
      2012 実施状況報告書
  • [学会発表] Rational term rewriting revisited: decidability and confluence2012

    • 著者名/発表者名
      Takahito Aoto and Jeroen Ketema
    • 学会等名
      6th International Conference on Graph Transformation
    • 発表場所
      Bremen, Germany
    • 関連する報告書
      2012 実施状況報告書
  • [学会発表] 減少ダイアグラム法による項書き換えシステムの可換性証明法2011

    • 著者名/発表者名
      的場正樹, 青戸等人, 外山芳人
    • 学会等名
      日本ソフトウェア科学会第28回大会
    • 発表場所
      那覇
    • 年月日
      2011-09-27
    • 関連する報告書
      2013 研究成果報告書
  • [学会発表] 永続性にもとづく項書き換えシステムの合流性証明2011

    • 著者名/発表者名
      鈴木翼, 青戸等人, 外山芳人
    • 学会等名
      日本ソフトウェア科学会第28回大会
    • 発表場所
      那覇
    • 年月日
      2011-09-27
    • 関連する報告書
      2013 研究成果報告書
  • [学会発表] 無限項書き換えシステムにおける性質に関する考察, 「代数と言語のアルゴリズムと計算理論」研究集会報告集, 数理解析研究所講究録2011

    • 著者名/発表者名
      岩見宗弘, 青戸等人
    • 発表場所
      京都大学数理解析研究所
    • 年月日
      2011-04-26
    • 関連する報告書
      2013 研究成果報告書
  • [備考]

    • URL

      http://www.nue.riec.tohoku.ac.jp/indexj.html

    • 関連する報告書
      2013 研究成果報告書
  • [備考]

    • URL

      http://www.nue.riec.tohoku.ac.jp/index-j.html

    • 関連する報告書
      2011 実施状況報告書

URL: 

公開日: 2011-08-05   更新日: 2019-07-29  

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

Powered by NII kakenhi