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

2013 年度 研究成果報告書

• 研究課題/領域番号: 23500002
• 研究種目: 基盤研究(C)
• 配分区分: 基金
• 応募区分: 一般
• 研究分野: 情報学基礎
• 研究機関: 東北大学
• 研究代表者: 青戸 等人 東北大学, 電気通信研究所, 准教授 (00293390)
• 研究分担者: 外山 芳人 東北大学, 電気通信研究所, 教授 (00251968)
• 研究期間 (年度): 2011 – 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)
  • 著者名/発表者名: 鈴木翼, 青戸等人, 外山芳人
  • 雑誌名: コンピュータソフトウェア 巻: Vol.30, No.3 ページ: 148-162
  • 査読あり
• [雑誌論文] 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)
  • 著者名/発表者名: 的場正樹, 青戸等人, 外山芳人
  • 雑誌名: コンピュータソフトウェア 巻: Vol.30, No.1 ページ: 187-202
  • 査読あり
• [雑誌論文] ボトムアップ書き換えに基づく最内書き換え到達可能性判定 (2013)
  • 著者名/発表者名: 高橋翔大, 青戸等人, 外山芳人
  • 雑誌名: 第15回プログラミングおよびプログラミング言語ワークショップ論文集
  • 査読あり
• [雑誌論文] 書き換え帰納法に基づく帰納的定理の決定可能性 (2013)
  • 著者名/発表者名: 中嶋辰成, 青戸等人, 外山芳人
  • 雑誌名: 第15回プログラミングおよびプログラミング言語ワークショップ論文集
  • 査読あり
• [雑誌論文] 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
  • 査読あり
• [雑誌論文] A reduction-preserving completion for proving confluence of non-terminating term rewriting systems (2012)
  • 著者名/発表者名: 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
  • 査読あり
• [雑誌論文] 無限項書き換えシステムにおける強頭部正規化可能性および一般生成性の自動反証 (2012)
  • 著者名/発表者名: 岩見宗弘, 青戸等人
  • 雑誌名: コンピュータソフトウェア 巻: Vol.29, No.1 ページ: 211-239
  • 査読あり
• [雑誌論文] 多項式サイズ正規形を保証する項書き換えシステムの経路順序 (2012)
  • 著者名/発表者名: 磯部耕己, 青戸等人, 外山芳人
  • 雑誌名: コンピュータソフトウェア 巻: Vol.29, No.1 ページ: 176-190
  • 査読あり
• [雑誌論文] 片側減少ダイアグラム法による項書き換えシステムの可換性証明法 (2012)
  • 著者名/発表者名: 的場正樹, 青戸等人, 外山芳人
  • 雑誌名: 第14回プログラミングおよびプログラミング言語ワークショップ論文集 ページ: 168-182
  • 査読あり
• [雑誌論文] 永続性にもとづく項書き換えシステムの合流性証明 (2012)
  • 著者名/発表者名: 鈴木翼, 青戸等人, 外山芳人
  • 雑誌名: 第14回プログラミングおよびプログラミング言語ワークショップ論文集 ページ: 153-167
  • 査読あり
• [雑誌論文] 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/
  • 査読あり
• [雑誌論文] 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/
  • 査読あり
• [雑誌論文] 多項式サイズ正規形を保証する項書き換えシステムの経路順序 (2011)
  • 著者名/発表者名: 磯部耕己, 青戸等人, 外山芳人
  • 雑誌名: 第13回プログラミングおよびプログラミング言語ワークショップ論文集 ページ: 99-113
  • 査読あり
• [雑誌論文] 基底項書き換え系の多項式時間合流性判定法の改良 (2011)
  • 著者名/発表者名: 村井正勝, 青戸等人, 外山芳人
  • 雑誌名: 第13回プログラミングおよびプログラミング言語ワークショップ論文集 ページ: 84-98
  • 査読あり
• [学会発表] 自動検証のためのプログラム変換 (2013)
  • 著者名/発表者名: 佐藤洸一, 菊池健太郎, 青戸等人, 外山芳人
  • 学会等名: 日本ソフトウェア科学会第30回大会
  • 発表場所: 東京
  • 年月日: 2013-09-13
• [学会発表] 閉包操作に基づく項書き換えシステムの到達可能性判定 (2013)
  • 著者名/発表者名: 四方駿作, 青戸等人, 外山芳人
  • 学会等名: 日本ソフトウェア科学会第30回大会
  • 発表場所: 東京
  • 年月日: 2013-09-13
• [学会発表] 永続性と減少ダイアグラム法に基づく合流性証明法 (2013)
  • 著者名/発表者名: 内田和真, 青戸等人, 外山芳人
  • 学会等名: 日本ソフトウェア科学会第30回大会
  • 発表場所: 東京
  • 年月日: 2013-09-13
• [学会発表] 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
• [学会発表] 木オートマトンに基づく項書き換えシステムの逆計算 (2012)
  • 著者名/発表者名: 椛澤涼, 青戸等人, 外山芳人
  • 学会等名: 日本ソフトウェア科学会第29回大会
  • 発表場所: 東京
  • 年月日: 2012-08-22
• [学会発表] ボトムアップ書き換えに基づく到達可能性の判定法 (2012)
  • 著者名/発表者名: 高橋翔大, 青戸等人, 外山芳人
  • 学会等名: 日本ソフトウェア科学会第29回大会
  • 発表場所: 東京
  • 年月日: 2012-08-22
• [学会発表] 書き換え帰納法に基づく帰納的定理の決定手続き (2012)
  • 著者名/発表者名: 中嶋辰成, 青戸等人, 外山芳人
  • 学会等名: 日本ソフトウェア科学会第29回大会
  • 発表場所: 東京
  • 年月日: 2012-08-22
• [学会発表] Transformations by templates for simply-typed term rewriting (2012)
  • 著者名/発表者名: Yuki Chiba and Takahito Aoto
  • 学会等名: Proceedings of the 6th International Workshop on Higher-Order Rewriting (HOR 2012)
  • 発表場所: Nagoya, Japan
  • 年月日: 2012-06-02
• [学会発表] 減少ダイアグラム法による項書き換えシステムの可換性証明法 (2011)
  • 著者名/発表者名: 的場正樹, 青戸等人, 外山芳人
  • 学会等名: 日本ソフトウェア科学会第28回大会
  • 発表場所: 那覇
  • 年月日: 2011-09-27
• [学会発表] 永続性にもとづく項書き換えシステムの合流性証明 (2011)
  • 著者名/発表者名: 鈴木翼, 青戸等人, 外山芳人
  • 学会等名: 日本ソフトウェア科学会第28回大会
  • 発表場所: 那覇
  • 年月日: 2011-09-27
• [学会発表] 無限項書き換えシステムにおける性質に関する考察, 「代数と言語のアルゴリズムと計算理論」研究集会報告集, 数理解析研究所講究録 (2011)
  • 著者名/発表者名: 岩見宗弘, 青戸等人
  • 発表場所: 京都大学数理解析研究所
  • 年月日: 2011-04-26
• [備考]
  • URL: http://www.nue.riec.tohoku.ac.jp/indexj.html