2011 年度研究成果報告書

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

研究課題

研究課題/領域番号	22700021
研究種目	若手研究(B)
配分区分	補助金
研究分野	ソフトウエア
研究機関	北海道大学
研究代表者	佐藤晴彦北海道大学, 大学院・情報科学研究科, 助教 (30543178)
研究期間 (年度)	2010 – 2011
キーワード	定理自動証明 / 項書換え系 / 帰納的定理証明
研究概要	ソフトウェアシステムの信頼性を高めるための基礎技術の一つである帰納的定理証明において,その自動化を推進するための効率の良い手続き及び推論戦略について研究した.複数の証明戦略を効率よく並列に実行するため,複数の並列動作に共通する処理を一括で実行する多重化の枠組みを用いた証明手続きを提案した.また証明の自動化において重要となる自動補題生成の実現に向け,正しい補題のみを生成する手法の基礎を構築した.

(4件)