リップリング法と書き換え帰納法を融合した定理自動証明法の研究

2010 年度 実績報告書

• 研究課題/領域番号: 20500002
• 研究機関: 東北大学
• 研究代表者: 青戸 等人 東北大学, 電気通信研究所, 准教授 (00293390)
• 研究分担者: 外山 芳人 東北大学, 電気通信研究所, 教授 (00251968)
• キーワード: 定理自動証明 / 書き換えシステム / リップリング / 書き換え帰納法 / 潜在帰納法

研究概要

本研究の目的は帰納的定理の自動証明法として項書き換えシステムに基づく暗黙的帰納法に着目し、その高度化を図ることである。このため明示的帰納法の強力なヒューリスティクスであるリップリング法を暗黙的帰納法へ応用するための基礎的な枠組みを構築した。正しさが保証されていない補題の導入する場合においても、補題の導入が証明手続きの流れを複雑にしてしまわないために、複数の証明プロセスを独立に動作させるための枠組みを形式化した。これにより、異なる複数の補題を独立に導入することが可能になり、補題の正しさが保証されていない場合にも見通しのよい動作が可能となった。さらに、潜在帰納法の鍵となる合流性証明法および到達可能性について実装システムを構築するとともに、前者については順序付け不能な等式を取り扱うことのできる新しい合流性証明法を考案し、後者については効果的な自動手続きについて検討を行った。

研究成果

• [雑誌論文] Automated confluence proof by decreasing diagrams based on rule-labelling (2010)
  • 著者名/発表者名: Takahito Aoto
  • 雑誌名: Proceedings of the 21st International Conference on Rewriting 巻: Vol.6 ページ: 7-16
  • 査読あり
• [雑誌論文] 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 ページ: 963-973
  • 査読あり
• [備考]
  • URL: http://www.nue.riec.tohoku.ac.jp/index-j.html