多重化に基づく,等式論理における帰納的定理証明の自動化

• 研究課題/領域番号: 22700021
• 研究種目: 若手研究(B)
• 配分区分: 補助金
• 研究分野: ソフトウエア
• 研究機関: 北海道大学
• 研究代表者: 佐藤 晴彦 北海道大学, 大学院・情報科学研究科, 助教 (30543178)
• 研究期間 (年度): 2010 – 2011
• 研究課題ステータス: 完了 (2011年度)
• 配分額: 1,300千円 (直接経費: 1,000千円、間接経費: 300千円); 2011年度: 650千円 (直接経費: 500千円、間接経費: 150千円); 2010年度: 650千円 (直接経費: 500千円、間接経費: 150千円)
• キーワード: 定理自動証明 / 項書換え系 / 帰納的定理証明

研究概要

ソフトウェアシステムの信頼性を高めるための基礎技術の一つである帰納的定理証明において,その自動化を推進するための効率の良い手続き及び推論戦略について研究した.複数の証明戦略を効率よく並列に実行するため,複数の並列動作に共通する処理を一括で実行する多重化の枠組みを用いた証明手続きを提案した.また証明の自動化において重要となる自動補題生成の実現に向け,正しい補題のみを生成する手法の基礎を構築した.

研究成果

• [雑誌論文] Multi-context rewriting induction with termination checkers (2010)
  • 著者名/発表者名: Haruhiko Sato, Masahito Kurihara
  • 雑誌名: IEICE Transactions on Information and Systems 巻: E93-D ページ: 942-952
  • NAID: 10026815209
  • 査読あり
• [学会発表] Recognition of Normal Forms for Sound Generalization (2011)
  • 著者名/発表者名: Haruhiko Sato
  • 学会等名: 35th TRS meeting
• [学会発表] 書き換え帰納法における文脈探索の有効性について (2011)
  • 著者名/発表者名: 佐藤晴彦
  • 学会等名: 情報処理学会第84回プログラミング研究発表会
• [学会発表] Optimizing mkbTT (System Description) (2010)
  • 著者名/発表者名: Sarah Winkler, Haruhiko Sato, Aart Middeldorp, Masahito Kurihara
  • 学会等名: 21st International Conference on Rewriting Techniques and Applications
  • 発表場所: エジンバラ大学,エジンバラ,イギリス
  • 年月日: 2010-07-13
• [学会発表] Optimizing mkbTT(System Description) (2010)
  • 著者名/発表者名: Sarah Winkler, Haruhiko Sato, Aart Middeldorp, Masahito Kurihara
  • 学会等名: 21st International Conference on Rewriting Techniques and Applications