2009 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 |
順序付け不能な等式を展開可能な書き換え帰納法の改良を行なった.まず,これから証明しようとする予想を用いた単純化の推論規則を導入することにより,健全補題生成法の導入規則の健全性の証明が可能になることが明らかにした.また,順序付け不能な等式の書き換え規則インスタンスや等価インスタンスの概念を導入することで,より見通しのよい推論体系の形式化を与えた.これらの改良に基づき,実験システムの改良を行なった.また,健全補代生成法や発散鑑定法を組み入れた帰納的定理自動証明の評価を行なった.
単純型付き項書き換えシステムに基づく高階関数をもつプログラムに対する帰納的定理証明法の実現を目指して,依存対手法に基づく単純型付き項書き換えシステムの停止性証明法の改良を行なった.単純型付き項書き換えシステムの依存対手法における引数フィルタリングおよび使用可能規則の理論を与えるとともに,実験システムの実装および実験による評価を行なった.
潜在帰納法による自動証明の鍵となる合流性自動判定についての研究については,昨年度に引き続き合流性検証システムACPの開発を行った。停止性をもたない項書き換えシステムについてはさまざまな合流条件が知られている.適用範囲の比較的広いと考えられる合流条件の実装を行った.このうち,減少ダイヤグラム法による合流性条件についてはルールラベリング法による条件が理論的には知られていたが,効率的な実装法が自明ではなかった.この問題を解決するためSMTソルバを用いて合流条件の判定を行う手法を提案した.
|
Research Products
(3 results)
