2016 Fiscal Year Research-status Report
帰納的定理証明の自動化に向けた補題生成と推論戦略の改良
| Project/Area Number |
16K16032
|
|---|
| Research Institution | Hokkai-Gakuen University |
|---|
Principal Investigator |
佐藤 晴彦 北海学園大学, 工学部, 准教授 (30543178)
|
|---|
| Project Period (FY) |
2016-04-01 – 2018-03-31
|
| Keywords | 帰納的定理証明 / 補題自動生成 / 書き換え帰納法 |
|---|
| Outline of Annual Research Achievements |
ソフトウェアシステムの性質を数学的な定理として論理的に証明することで極めて高い信頼性・安全性を確保する形式手法において、人手による証明が高コスト及び困難となることが実用上の障害となっている。このため計算機により自動的に定理を証明する、自動証明システムの適用範囲の拡大が重要な課題となっている。本研究では定理証明問題のうち特に自動化が困難であると知られている証明に帰納法を要する種類の定理（帰納的定理）を対象とし、その証明の自動化において重要となる補題の自動生成について研究を行った。平成28年度は具体的には以下の研究を行った。
（１）書き換え帰納法を用いた帰納的定理の補題自動生成手法の提案
補題の自動生成における先行手法として、補題候補の集合について網羅的に証明を試みる手法が提案されていたが、先行手法では証明に用いる帰納法の枠組みとして単純な構造帰納法のみを用いており、より複雑な証明を要する補題を生成できない問題点があった。この問題に対し、より強力かつ柔軟な帰納法の枠組みである書き換え帰納法を用いる手法を提案した。実験により手法の有効性が確認されると共に、より複雑な定理の証明を成功させるには前段階での補題候補の集合生成手法の改善も必要となることが分かった。
（２）正しい一般化による補題生成に向けた、関数の値域集合を求める手続きの検討
有効な補題は既知の補題の一部を適切に一般化することで得られる場合があるため、一般化の正しさを保証する手法の実現が重要となる。関数が取り得る値の集合（値域集合）の計算に基づく一般化手法において、複雑な関数に対してはこの計算が発散する場合があることが問題となっていた。この問題に対し、特定の問題における発散の様子を分析し、その発散を収束させる手続きの実現方法を検討した。
|
| Current Status of Research Progress |
Current Status of Research Progress
3: Progress in research has been slightly delayed.
Reason
当初は書き換え帰納法を用いた補題生成手法について、その補題を利用した主定理の証明を試みる一般の証明手続きへの組み込みに取り組むものとしていたが、組み込み前の予備実験により、当初予期していたよりも補題生成手法の能力が十分でなく主定理の証明のための補題が十分に得られない場合が多いことが分かったため、平成28年度は手法自体の更なる改善を試みた。このため当初の計画より進捗が遅れている。
|
| Strategy for Future Research Activity |
平成29年度も引き続き書き換え帰納法を用いた補題自動生成手法の能力向上に向け、特に補題候補集合の生成手法の改善という観点から研究を進める。加えてそれらの手法を組み込んだ帰納的定理証明システムを実装し、その評価と改善に取り組む。
|
| Causes of Carryover |
当初の予定より国際会議の参加に要する旅費が抑えられ、また実験に用いる計算機等の物品の購入も平成28年度は行う必要がなかったため、余りが生じた。
|
| Expenditure Plan for Carryover Budget |
必要に応じて、研究発表のための出張費用および実験に用いる計算機や記憶装置等の物品購入費用の補助に用いる。
|
