| 研究課題/領域番号 |
10680346
|
|---|
| 研究機関 | 東北大学 |
|---|
研究代表者 |
外山 芳人 東北大学, 電気通信研究所, 教授 (00251968)
|
|---|
| 研究分担者 |
草刈 圭一郎 東北大学, 電気通信研究所, 助手 (90323112)
鈴木 大郎 東北大学, 電気通信研究所, 助手 (90272179)
|
|---|
| キーワード | 項書き換えシステム / 自動証明 / 潜在帰納法 / 書き換え帰納法 |
|---|
| 研究概要 |
新しいプログラム検証技術の形式的な基礎を与える目的で、項書き換えシステムに基づく帰納的定理の自動証明手法である潜在帰納法と書き換え帰納法の差異を解析するとともに、自動証明に有効な関連手法を研究し以下の成果を得た。
(1)潜在帰納法と書き換え帰納法にそれぞれ反駁証明法を組み合わせた証明能力の等価性について理論的に解析し、それぞれの証明手法の実装上の違いが具体的な自動証明の能力に影響を与えていることを明らかにした。
(2)定理自動証明やプログラムの正当性検証で重要なリダクションの停止条件について解析し、従来提案されていた依存対による停止性判定手法が結合律と交換律をもつような関数に対しても拡張できることを示した。
(3)項書き換えシステムの自動合成の実験を行い、完備化手続きをもちいることによって融合変換にもとづくプログラムの自動合成が可能であることを明らかにした。
|
