2010 Fiscal Year Annual Research Report
多重化に基づく、等式論理における帰納的定理証明の自動化
| Project/Area Number |
22700021
|
|---|
| Research Institution | Hokkaido University |
|---|
Principal Investigator |
佐藤 晴彦 北海道大学, 大学院・情報科学研究科, 助教 (30543178)
|
|---|
| Keywords | 定理自動証明 / 項書換え系 / 帰納的定理証明 |
|---|
| Research Abstract |
本研究では、ソフトウェアシステムの信頼性を高めるための基礎技術の一つである、帰納的定理証明において、その自動化を推進するための効率の良い手続き及び推論戦略について研究を行った。具体的には、等式論理における、証明に帰納法を要する種類の定理(帰納的定理)の証明原理の一つである書き換え帰納法について、その自動化及び効率化に取り組んだ。書き換え帰納法は項書換え系の理論に基づく証明原理であり、可能となる推論の構造が完備化手続きと類似しているため、完備化手続きの自動化の手法が適用可能である。平成22年度はこの手法の適用に関する下記2点の研究を実施した。
(1)多重化に基づぐ強力な書き換え帰納法手続きの提案
書き換え帰納法における重要なパラメータである簡約順序について、それについての制約を保持し潜在的な多数の簡約順序を並列的に取り扱えるように多重化し、自動証明可能な範囲を広げた手続きを提案した。また、本質的に等価な制約や推論上有用でない制約を自動検出することで考慮すべき制約を削減し高速化するための原理を提案した。
(2)適切な推論戦略の自動選択の実現に向けた、基礎理論の講築と実験
帰納的定理の証明を成功させるには、書き換え規則の適用順序の選択や適切な補題の追加といった非決定的な推論が重要であり、探索範囲を現実的なサイズに制限するには適切な推論戦略を設定する必要がある。本研究では多数の例に対する実験を通して書き換え規則の適切な適用順序を検討した。また決定可能な帰納的定理のクラスに関する既存の研究成果に基づき,正当性の検証が容易かつ有用性の高い補題の特徴付けを行った。
|
Research Products
(2 results)
