2017 Fiscal Year Annual Research Report
Improvement of lemma generation and reasoning strategies for automated inductive theorem proving
| 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 |
ソフトウェアシステムの性質を数学的な定理として論理的に証明することで極めて高い信頼性・安全性を確保する形式手法において、人手による証明が高コスト及び困難となることが実用上の障害となっている。このため計算機により自動的に定理を証明する、自動証明システムの適用範囲の拡大が重要な課題となっている。本研究では定理証明問題のうち特に自動化が困難であると知られている証明に帰納法を要する種類の定理（帰納的定理）を対象とし、その証明の自動化において重要となる補題の自動生成について研究を行った。平成29年度は具体的には以下の研究を行った。
（１）発散鑑定と一般化に基づく補題生成手法の提案
証明において帰納法の適用が無限に繰り返され停止しない（発散する）際、補題の一部分を一般化することが多くの場合有効であるが、補題を非定理とする過度な一般化を避けることが課題であった。これに対し、既存の手続きにより求められる発散の形式に基づき、一般化の対象とする部分を制限することで有望な一般化を得るヒューリスティックを提案し、実験によってその有効性を確認した。
（２）書き換え帰納法を用いた帰納的定理の補題自動生成手法の提案
前年度に提案した、書き換え帰納法に基づく網羅的な補題自動生成（定理自動発見）の手法を用いてより難しい性質を対象とした実験を行い、その中で現状の手法が発見できていない重要な補題を分析しその解決策を検討した。特に、構文的に複雑であるがある種の一般性を持つ有用な補題が、現状の構文的に単純なものから順に探索する手法では発見が困難であることを示した。またこの問題に対し、導出可能性に基づいた相対的な有用性等を利用した補題候補生成段階での改善手法を検討した。
|
