2010 Fiscal Year Annual Research Report
リップリング法と書き換え帰納法を融合した定理自動証明法の研究
| Project/Area Number |
20500002
|
|---|
| Research Institution | Tohoku University |
|---|
Principal Investigator |
青戸 等人 東北大学, 電気通信研究所, 准教授 (00293390)
|
|---|
| Co-Investigator(Kenkyū-buntansha) |
外山 芳人 東北大学, 電気通信研究所, 教授 (00251968)
|
|---|
| Keywords | 定理自動証明 / 書き換えシステム / リップリング / 書き換え帰納法 / 潜在帰納法 |
|---|
| Research Abstract |
本研究の目的は帰納的定理の自動証明法として項書き換えシステムに基づく暗黙的帰納法に着目し、その高度化を図ることである。このため明示的帰納法の強力なヒューリスティクスであるリップリング法を暗黙的帰納法へ応用するための基礎的な枠組みを構築した。正しさが保証されていない補題の導入する場合においても、補題の導入が証明手続きの流れを複雑にしてしまわないために、複数の証明プロセスを独立に動作させるための枠組みを形式化した。これにより、異なる複数の補題を独立に導入することが可能になり、補題の正しさが保証されていない場合にも見通しのよい動作が可能となった。さらに、潜在帰納法の鍵となる合流性証明法および到達可能性について実装システムを構築するとともに、前者については順序付け不能な等式を取り扱うことのできる新しい合流性証明法を考案し、後者については効果的な自動手続きについて検討を行った。
|
