2015 Fiscal Year Annual Research Report
代数的ソフトウェア向き多重文脈型推論基盤システムによる帰納的定理証明とその応用
| Project/Area Number |
25330074
|
|---|
| Research Institution | Hokkaido University |
|---|
Principal Investigator |
栗原 正仁 北海道大学, 情報科学研究科, 教授 (50133707)
|
|---|
| Project Period (FY) |
2013-04-01 – 2016-03-31
|
| Keywords | 項書換え系 / 帰納的定理証明 / 代数的ソフトウェア / 多重文脈型推論 |
|---|
| Outline of Annual Research Achievements |
文脈が互いに類似した非決定性並行プロセス間には，多くの場合，同一の計算・推論の処理が多数共通に存在する。本研究はそれらを共通に処理することによってシステム性能を飛躍的に高めることを狙った多重文脈型推論の基盤を開発するという全体構想の中で，帰納的定理の自動証明を行う多重文脈型推論システムを開発すること及びそれを代数的ソフトウェアの正しさの検証に応用してその可用性を高めることを目的としている。具体的には，項書換え系として知られる代数的ソフトウェアに関する研究分野を中心として，等式や書換え規則に関わる推論（停止性検証，完備化，定理証明等）を取り扱うシステムの研究開発を進める。
平成25年度に主として基礎技術の調査とシステムの計画に係る研究を推進し，平成26年度と27年度に主要な研究成果を創出した。その概略は以下の通りである。
１．本研究費で購入した並列計算機システムの上で，関数型オブジェクト指向プログラミング言語SCALAを用い，多重文脈型推論基盤システムを再実装し，その上で停止性検証，完備化，帰納的定理証明を効率良く実行するシステムを開発した。
２．代数的ソフトウェアの正しさの検証に関わる標準的なベンチマーク問題に本システムを適用し，所定の制限時間内に，従前よりも文脈を適切に探索して推論に成功することを確認した。
３．特に探索に関わる人工知能技術とヒューリスティックスを組み合わせることによって，本システムの重要部分である停止性自動証明の並列計算機上での実装技術を開発し，効率を向上させた。その成果は査読付き論文として国際的な論文誌において公表している。また，本システムの複雑化を防ぎつつさらに効率を改善するために，SCALAの遅延評価機構を効果的に活用した実装技術を開発した。その成果は査読付き論文として国際会議において公表している。
|
