| 研究課題/領域番号 |
16K00090
|
|---|
| 研究機関 | 北海道大学 |
|---|
研究代表者 |
栗原 正仁 北海道大学, 情報科学研究科, 教授 (50133707)
|
|---|
| 研究期間 (年度) |
2016-04-01 – 2019-03-31
|
| キーワード | 帰納的定理証明 / 補題生成 / 項書換え系 / 書換え帰納法 / 多重文脈推論 |
|---|
| 研究実績の概要 |
文脈（計算開始から現時点までに行った選択の列）が互いに類似した非決定性並行プロセス間には，多くの場合，同一の計算・推論の処理が多数共通に存在する。本研究は，それらを共通に処理することによってシステム性能を飛躍的に高めることを狙った「多重文脈型推論」の基盤を開発するという全体構想の中で，(1) 補助定理を自動生成して帰納的定理の自動証明を行う多重文脈型推論システムを開発すること，及び(2)それを代数的ソフトウェアの正しさの検証に応用してその可用性を高めること，を目的としている。
平成28年度までには要素技術とシステム計画に係る調査研究を進め，補助定理を自動生成する手法（トップダウン的な手法，ボトムアップ的な手法）の調査，及びそれらを多重文脈型推論システムとして総合化するシステムの基本的骨組みを計画し，その一部の研究成果として，ボトムアップ的な手法と書き換え帰納法の組合せによる補助定理自動生成手法を提案し，国際会議(IEEE SMC 2016)において発表した。
平成29年度は，まず前年度に引き続いて上記のボトムアップ的な手法について検討を深め，これまでよりも構文的に複雑な補助定理の有効性とその自動生成手法について，基本的な議論を行い，国際会議（IAENG IMECS 2018）において発表した。一方，実装のプラットフォームとして，本研究経費の設備備品費で購入した並列計算機システムを用い，前年度の計画に基づいて，システムの設計・実装に関しても研究を進めた。また，理論的な研究成果として，トップダウン的な補助定理自動生成手法を新規に１つ提案し，書き換え帰納法と多重文脈型推論の組み合わせの枠組みでそれを実装して動作を確認するとともに，代数的ソフトウェアの正しさの検証への応用分野においてその有効性を確認し，この研究成果を英文論文として取りまとめ，論文誌に投稿した（現在査読中）。
|
| 現在までの達成度 (区分) |
現在までの達成度 (区分)
2: おおむね順調に進展している
理由
補助定理を自動生成する手法として，２つの代表的なアプローチ（トップダウン的な手法，ボトムアップ的な手法）で研究を進め，ボトムアップ的な手法については平成28年度から29年度にかけて，基本的な研究成果が得られ，２つの国際会議において発表している。また，トップダウン的な手法については，平成29年度に理論的に新しい研究成果が得られ，学術論文として投稿中である。いずれの研究においても，代数的ソフトウェアの正しさの検証分野に応用してその有効性を確かめていることから，本研究課題は，おおむね順調に進展していると判断している。
|
| 今後の研究の推進方策 |
平成30年度は，現行の多重文脈型推論システムでこれまで解けなかった標準問題を用いて，開発したシステムの性能評価を行い，必要に応じて設計・実装の改善を行う。これまでと同様に，応用分野であるプログラム検証の分野特有の問題群を用いて，開発したシステムの可用性の評価を行い，必要に応じて設計・実装の改善を行う。そして本研究の成果を総括し，論文等により公表するほか，ホームページ等においてアイデアの原理やその社会的意義等について啓発を行う。
なお，連携研究者の佐藤晴彦は，引き続き，実装および評価に係る研究に関して連携協力を行う。また，システムの具体的な実装と評価実験は，引き続き研究協力者（大学院生１名）が行うことを想定する。
|
| 次年度使用額が生じた理由 |
購入した備品（並列計算機）が当初の研究計画時の見積り金額より安価となった。また，国際会議への旅費を研究協力者２名の分も含めて計上していたが，実際にはそのうち１名は本助成金ではない予算を使用し，別の１名は都合により不参加となったため，およそこれに相当する分の予算が余ることとなった。この予算は，次年度の追加的な備品購入および国際会議への旅費および他の直接的経費として有効に活用することとしたい。
|
