| 研究課題/領域番号 |
25330074
|
|---|
| 研究種目 |
基盤研究(C)
|
| 配分区分 | 基金 |
|---|
| 応募区分 | 一般 |
|---|
| 研究分野 |
ソフトウェア
|
|---|
| 研究機関 | 北海道大学 |
|---|
研究代表者 |
栗原 正仁 北海道大学, 情報科学研究科, 教授 (50133707)
|
|---|
| 連携研究者 |
佐藤 晴彦 北海道大学, 大学院情報科学研究科, 助教 (30543178)
|
|---|
| 研究協力者 |
季 承成
高松 宏樹
丁 睿
|
|---|
| 研究期間 (年度) |
2013-04-01 – 2016-03-31
|
| 研究課題ステータス |
完了 (2015年度)
|
| 配分額 *注記 |
5,070千円 (直接経費: 3,900千円、間接経費: 1,170千円)
2015年度: 650千円 (直接経費: 500千円、間接経費: 150千円)
2014年度: 3,770千円 (直接経費: 2,900千円、間接経費: 870千円)
2013年度: 650千円 (直接経費: 500千円、間接経費: 150千円)
|
|---|
| キーワード | 項書換え系 / 帰納的定理自動証明 / 多重文脈推論 / 代数的ソフトウェア / 代数的仕様記述 / システム形式検証 / 帰納的定理証明 / 多重文脈型推論 |
|---|
| 研究成果の概要 |
並列計算機上で多重文脈型推論基盤システムを開発し，停止性検証，完備化，帰納的定理証明を効率良く実行するシステムを開発した。代数的ソフトウェアの正しさの検証に関わる標準的なベンチマーク問題について，従前よりも文脈を適切に探索して推論に成功することと，従前のシステムでは解けなかった問題が，補助定理を自動生成することで解けることを確認した。
探索に関わる人工知能技術とヒューリスティクスを組み合わせることによって，本システムの重要部分である停止性自動検証の並列計算機上での実装技術を開発し，効率を向上させた。また，プログラミング言語SCALAのもつ遅延評価機構を用いて，システムの実行効率を改善した。
|
