研究課題
若手研究(B)
ソフトウェアシステムの性質を数学的な定理として論理的に証明することで極めて高い信頼性・安全性を確保する形式手法において、人手による証明が高コスト及び困難となることが実用上の障害となっている。このため計算機により自動的に定理を証明する、自動証明システムの適用範囲の拡大が重要な課題となっている。本研究では定理証明問題のうち特に自動化が困難であると知られている証明に帰納法を要する種類の定理（帰納的定理）を対象とし、その証明の自動化において重要となる補題の自動生成について新しい手法を提案した。
ソフトウェア科学
