2011 Fiscal Year Annual Research Report
多重化に基づく、等式論理における帰納的定理証明の自動化
| Project/Area Number |
22700021
|
|---|
| Research Institution | Hokkaido University |
|---|
Principal Investigator |
佐藤 晴彦 北海道大学, 大学院・情報科学研究科, 助教 (30543178)
|
|---|
| Keywords | 定理自動証明 / 項書換え系 / 帰納的定理証明 |
|---|
| Research Abstract |
本研究では、ソフトウェアシステムの信頼性を高めるための基礎技術の一つである、帰納的定理証明において、その自動化を推進するための効率の良い手続き及び推論戦略について研究を行った。具体的には、等式論理における、証明に帰納法を要する種類の定理(帰納的定理)の証明原理の一つである書き換え帰納法について、その自動化及び効率化に取り組んだ。書き換え帰納法は項書換え系の理論に基づく証明原理であり、可能となる推論の構造が完備化手続きと類似しているため、完備化手続きの自動化の手法が適用可能である。平成23年度はこの手法の適用に関する下記2点の研究を実施した。
(1)多重化に基づく書き換え帰納法手続きへの自動補題生成手法の導入
証明の自動化においては適切な補題の追加が極めて重要である。書き換え帰納法における有効性が確かめられている自動補題生成手続きの一つに発散鑑定法に基づく一般化が知られている。前年度に提案した多重化に基づく書き換え帰納法手続きにこの発散鑑定法に基づく一般化手続きを導入し、その有効性を調べた。実験により、多重化による帰納法の枠組みの探索と補題生成の組み合わせにより自動証明が容易となる例が発見された。
(2)健全な等式変換に関する理論の構築と、そのための正規形集合の認識手続きの実現
補題生成手法の一つである発散鑑定法は等式の一般化を基礎としているが、それにより補題の正しさが失われる可能性がある。正しさを保存する健全な一般化を実現するため、等式中のある部分が取り得る計算結果全体を表す正規形集合の同一性に基づく健全な一般化の理論を構築した。またその同一性判定手続きを実現するため、正規形集合を認識する木オートマトンを構成し、木オートマトンの同一性判定手続きに帰着させる手続きを提案した。
|
