| 研究課題/領域番号 |
16K16032
|
|---|
| 研究種目 |
若手研究(B)
|
| 配分区分 | 基金 |
|---|
| 研究分野 |
ソフトウェア
|
|---|
| 研究機関 | 北海学園大学 |
|---|
研究代表者 |
佐藤 晴彦 北海学園大学, 工学部, 准教授 (30543178)
|
|---|
| 研究期間 (年度) |
2016-04-01 – 2018-03-31
|
| 研究課題ステータス |
完了 (2017年度)
|
| 配分額 *注記 |
1,300千円 (直接経費: 1,000千円、間接経費: 300千円)
2017年度: 650千円 (直接経費: 500千円、間接経費: 150千円)
2016年度: 650千円 (直接経費: 500千円、間接経費: 150千円)
|
|---|
| キーワード | 定理自動証明 / 帰納的定理証明 / 補題自動生成 / 書き換え帰納法 / 項書換え系 / 形式的検証 |
|---|
| 研究成果の概要 |
ソフトウェアシステムの性質を数学的な定理として論理的に証明することで極めて高い信頼性・安全性を確保する形式手法において、人手による証明が高コスト及び困難となることが実用上の障害となっている。このため計算機により自動的に定理を証明する、自動証明システムの適用範囲の拡大が重要な課題となっている。本研究では定理証明問題のうち特に自動化が困難であると知られている証明に帰納法を要する種類の定理（帰納的定理）を対象とし、その証明の自動化において重要となる補題の自動生成について新しい手法を提案した。
|
