| 研究課題/領域番号 |
16K00090
|
|---|
| 研究種目 |
基盤研究(C)
|
| 配分区分 | 基金 |
|---|
| 応募区分 | 一般 |
|---|
| 研究分野 |
ソフトウェア
|
|---|
| 研究機関 | 北海道大学 |
|---|
研究代表者 |
栗原 正仁 北海道大学, 情報科学研究科, 教授 (50133707)
|
|---|
| 研究協力者 |
佐藤 晴彦
|
|---|
| 研究期間 (年度) |
2016-04-01 – 2019-03-31
|
| 研究課題ステータス |
完了 (2018年度)
|
| 配分額 *注記 |
4,810千円 (直接経費: 3,700千円、間接経費: 1,110千円)
2018年度: 650千円 (直接経費: 500千円、間接経費: 150千円)
2017年度: 3,510千円 (直接経費: 2,700千円、間接経費: 810千円)
2016年度: 650千円 (直接経費: 500千円、間接経費: 150千円)
|
|---|
| キーワード | 帰納的定理 / 定理自動証明 / 定理自動発見 / 補題生成 / 多重文脈型推論 / 代数的ソフトウェア / 項書換え系 / 帰納的定理自動証明 / 書換え帰納法 / 多重文脈推論 / 帰納的定理証明 / 補助定理 / 定理発見 / 発散鑑定 / 仕様記述・検証 |
|---|
| 研究成果の概要 |
本研究は，多重文脈型推論システムと呼ばれる新しい考え方のシステム構造を用いて，計算機科学および計算機工学において重要な役割を果たす帰納的定理と呼ばれる種類の数学的定理の発見や証明を自動的かつ効率的に行う技術を開発することを全体構想とし，その目的を達成するため，主定理を証明する際に必要となる補助定理を自動的に生成するためのトップダウン的及びボトムアップ的な新しい方法に基づいて総合的に検討を行い，システムの開発を行うとともに，応用として想定されるソフトウェア工学における代数的ソフトウェアの正しさの検証の分野において適用可能であることを実証的に確認したものである。
|
| 研究成果の学術的意義や社会的意義 |
ソフトウェア工学の理論的基礎分野では，作成したソフトウェアの正しさを機械的に確認する技術が重要視されている。そのため代数的にソフトウェアの仕様を記述して実装する技術が考案されており，そこではソフトウェアの正しさを数学的な帰納的定理の証明に帰着させ，それを計算機により自動的に証明するアプローチを採っている。本研究成果はそのような技術開発に対して有益な知見を提供する点に学術的意義があるとともに，最終的にはソフトウェアの正しさの保証を通じて，安心・安全な情報社会の実現に寄与し得る点に社会的意義が認められる。
|
