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

2008 Fiscal Year Annual Research Report

• Project/Area Number: 20500002
• Research Institution: Tohoku University
• Principal Investigator: 青戸 等人 Tohoku University, 電気通信研究所, 准教授 (00293390)
• Co-Investigator(Kenkyū-buntansha): 外山 芳人 東北大学, 電気通信研究所, 教授 (00251968)
• Keywords: 定理自動証明 / 書き換えシステム / リップリング / 書き換え帰納法 / 潜在帰納法 / 健全一般化法 / 発散鑑定法 / 合流性

Research Abstract

リップリング法を暗黙的帰納法に取り入れる上で問題となる点の1つとして、書き換え帰納法において定理の展開が従来不可能である場合に着目してその解決を図った。仮定に厳密な順序や等価な順序がつかない場合にも仮定が適用可能となるような書き換え帰納法の拡張を考案した。その設計に基づく帰納的定理証明システムを実装しその有効性を問題点を確かめた。停止性検証機能を拡張書き換え帰納法へ取り入れる際、用いる簡約順序が基底全順序とならない問題が見つかり、その点を改善した部分システムを設計した。
帰納的定理の自動証明においては、適切な補題の発見が証明成功の鍵である。このため、さまざまな補題自動生成法が考案されている。上記の証明システムに発散鑑定法や健全一般化法といった補題発見法を組み込んだ。健全一般化法については、従来与えられていた条件の誤りを発見し反例を与えるとともに、その他の条件を一般化し、より広範囲に適用可能な健全一般化法の提案を行なった。
潜在帰納法による自動証明の鍵となる合流性自動判定法について、従来のさまざまな合流性判定条件を統合した検証システムを設計・構築した。実現した検証システムは合流性を保証する複数の条件の検証と、部分システムの合流・非合流性から全体の合流・非合流性を判定する合流性のモジュラー性にもとづく。これにより単一の条件では合流性の判定が困難な例に対しても、複数の条件を組み合わせた合流性の検証が可能である。また、最内停止性証明に基づく判定法や非合流性検証条件を提案し、これを合流性検証システムに組み入れた。