定理自動証明に基づくプログラム変換システムの研究

2009 年度 研究成果報告書

• 研究課題/領域番号: 19500003
• 研究種目: 基盤研究(C)
• 配分区分: 補助金
• 応募区分: 一般
• 研究分野: 情報学基礎
• 研究機関: 東北大学
• 研究代表者: 外山 芳人 東北大学, 電気通信研究所, 教授 (00251968)
• 研究分担者: 青戸 等人 東北大学, 電気通信研究所, 准教授 (00293390)
• 研究期間 (年度): 2007 – 2009
• キーワード: プログラム理論 / プログラム変換

研究概要

定理自動証明や計算モデルで広く利用されている項書き換えシステムの理論に基づいて、プログラム自動変換を実現するための基礎理論と実験システムを開発した。研究成果としては、プログラム変換のための変換パターン自動抽出アルゴリズムの提案と実験システムの構築、高階プログラムの新しい停止性証明法の提案、書き換え帰納法のための補題自動導入アルゴリズムの提案と実験システムの構築、分割統治法による項書き換えシステムの合流性自動判システムの開発を行った。

研究成果

• [雑誌論文] Program transformation templates for tupling based on term rewriting (2010)
  • 著者名/発表者名: Yuki Chiba, Takahito Aoto, Yoshihito Toyama
  • 雑誌名: IEICE Transactions on Information and Systems Vol.E93-D、No.5 ページ: 963-973
  • 査読あり
• [雑誌論文] Argument filterings and usable rules for simply typed dependency pairs (2009)
  • 著者名/発表者名: Takahito Aoto, Toshiyuki Yamada
  • 雑誌名: LNAI Vol.5749 ページ: 117-132
  • 査読あり
• [雑誌論文] Proving confluence of term rewriting systems automatically (2009)
  • 著者名/発表者名: Takahito Aoto, Junichi Yoshida, Yoshihito Toyama
  • 雑誌名: LNCS Vol.5595 ページ: 93-102
  • 査読あり
• [雑誌論文] 項書き換えシステムの合流性自動判定 (2009)
  • 著者名/発表者名: 吉田順一, 青戸等人, 外山芳人
  • 雑誌名: コンピュータソフトウェア Vol.26、No.2 ページ: 76-92
  • 査読あり
• [雑誌論文] 反証機能付き書き換え帰納法のための補題自動生成法 (2009)
  • 著者名/発表者名: 嶌津聡志, 青戸等人, 外山芳人
  • 雑誌名: コンピュータソフトウェア Vol.26、No.2 ページ: 41-55
  • 査読あり
• [雑誌論文] Modular Church-Rosser Modulo : The Complete Picture (2008)
  • 著者名/発表者名: Jean-Pierre Jouannaud, Yoshihito Toyama
  • 雑誌名: International Journal of Software and Informatics Vol.2、No.1 ページ: 61-75
  • 査読あり
• [雑誌論文] Termination proof of S-expression rewriting systems with recursive path relations (2008)
  • 著者名/発表者名: Yoshihito Toyama
  • 雑誌名: LNCS Vol.5117 ページ: 381-391
  • 査読あり
• [雑誌論文] Soundness of rewriting induction based on an abstract principle (2008)
  • 著者名/発表者名: Takahito Aoto
  • 雑誌名: IPSJ Transactions on Programming Vol.49、No.SIG 1(PRO 35) ページ: 28-38
  • 査読あり
• [雑誌論文] Automatic construction of program transformation templates (2008)
  • 著者名/発表者名: Yuki Chiba, Takahito Aoto, Yoshihito Toyama
  • 雑誌名: IPSJ Transactions on Programming Vol.49、No.SIG 1(PRO 35) ページ: 14-27
  • 査読あり
• [学会発表] 帰納的経路関係に基づくS式書き換えシステムの停止性証明 (2007)
  • 著者名/発表者名: 外山芳人
  • 学会等名: 日本ソフトウェア科学会第24回大会
  • 発表場所: 奈良先端科学技術大学院大学
  • 年月日: 2007-09-13
• [学会発表] 停止性検証器を利用した書き換え帰納法手続き (2007)
  • 著者名/発表者名: 青戸等人
  • 学会等名: 日本ソフトウェア科学会第24回大会
  • 発表場所: 奈良先端科学技術大学院大学
  • 年月日: 2007-09-13
• [備考] ホームページ等
  • URL: http://www.nue.riec.tohoku.ac.jp/index-j.html