2013 Fiscal Year Research-status Report
代数的ソフトウェア向き多重文脈型推論基盤システムによる帰納的定理証明とその応用
| Project/Area Number |
25330074
|
|---|
| Research Category |
Grant-in-Aid for Scientific Research (C)
|
| Research Institution | Hokkaido University |
|---|
Principal Investigator |
栗原 正仁 北海道大学, 情報科学研究科, 教授 (50133707)
|
|---|
| Project Period (FY) |
2013-04-01 – 2016-03-31
|
| Keywords | 項書換え系 / 帰納的定理証明 / 代数的ソフトウェア / 多重文脈型推論 |
|---|
| Research Abstract |
文脈が互いに類似した非決定性並行プロセス間には，同一の計算・推論の処理が多数共通に存在する。本研究は，それらの共通処理によってシステム性能を飛躍的に高めることを狙った多重文脈型推論の基盤を開発するという全体構想の中で，補助定理を自動生成して帰納的定理の自動証明を行う多重文脈型推論システムを開発すること，及びそれを代数的ソフトウェアの正しさの検証に応用してその可用性を高めることを目的とする。具体的には，ソフトウェア工学と人工知能の境界領域内の項書換え系として知られる代数的ソフトウェアに関する研究分野を中心として，等式や書換え規則に関わる推論を取り扱うシステムの研究開発を進める。様々な人工知能技術とヒューリスティックスを使い，基礎から実装そして応用へつなげることを目的とする。
平成25年度には，主として基礎技術の調査とシステムの計画に係る研究を推進した。項書換え系分野における補助定理の生成や帰納的定理の証明・発見の基礎技術の調査を行い，それらから本研究の目的に適したものを取捨選択し，システムを計画した。
（１）項書換え系分野における帰納的定理の証明に関する調査を行い，その特徴を整理した。
（２）定理の発見の基礎技術の調査を行い，その特徴を整理した。
（３）基礎技術の取捨選択とシステム計画を行った。具体的には，上記（１）と（２）で調査・整理した種々の基礎技術の特徴に基づき，帰納的定理証明の観点から，多重文脈型推論システムの目的及び特徴に照らし合わせて，木オートマトンにより正規形を認識する観点に着目して理論的検討を行った。また，システムを高機能な関数型言語などで実装し直して，今後のシステムの複雑化に対処したり，マルチコアCPUを用いて並列実行させることも考慮しつつ，オブジェクト指向プログラムの自動テストの環境を開発した。
|
| Current Status of Research Progress |
Current Status of Research Progress
2: Research has progressed on the whole more than it was originally planned.
Reason
研究の目的に照らして事前に計画したとおり，平成25年度には，主として基礎技術の調査とシステムの計画に係る研究を推進し，項書換え系分野における補助定理の生成や帰納的定理の証明・発見の基礎技術の調査を行い，それらから本研究の目的に適したものを取捨選択し，システムを計画した。具体的には，項書換え系分野における帰納的定理の証明に関する調査を行い，定理の発見の基礎技術の調査を行い，それらの特徴を整理した。また，基礎技術の取捨選択とシステム計画の一環として，調査・整理した種々の基礎技術の特徴に基づき，帰納的定理証明の観点から，多重文脈型推論システムの目的及び特徴に照らし合わせて，木オートマトンにより正規形を認識する観点に着目して理論的検討を行った。また，システムを高機能な関数型言語などで実装し直して，今後のシステムの複雑化に対処したり，マルチコアCPUを用いて並列実行させることも考慮しつつ，オブジェクト指向プログラムの自動テストの環境を開発した。これらの成果については，国際会議において公表している。
|
| Strategy for Future Research Activity |
平成26年度は，平成25年度の研究実績で示した（１），（２），（３）を引き続き実施すると共に，実装のプラットフォームとして，本研究経費の設備備品費で購入するマルチコアの並列計算機システムを用いることとし，前年度のシステム計画に基づいて，システムの設計・実装に関して研究を進める。システムが正しく帰納的定理証明を実行することを確認すると共に，予備的な評価を実施し，ここまでの中間成果をとりまとめて発表し，広くコメントや助言を求めるようにする。また，主要な国際会議で発表される最新の技術動向を調査することなどを含めて検討する。
平成27年度は，帰納的定理証明に関する標準問題を用いて，開発したシステムの性能評
価を行い，必要に応じて設計・実装の改善を行う。また，応用分野であるプログラム検証やソフトウェアテストの分野について調査を行い，その分野特有の問題群を用いて，開発したシステムの可用性の評価を行い，必要に応じて設計・実装の改善を行う。そして本研究の成果を総括し，論文等により公表するほか，ホームページ等においてアイデアの原理
等について啓発を行う。
なお，連携研究者の佐藤晴彦は，引き続き本研究に係る連携研究を行う。
|
| Expenditure Plans for the Next FY Research Funding |
「その他」として計上していた国際会議参加費が予想より高額であったため，物品費および謝金に相当する支出については，節約的に行いつつ，翌年度でも可能な支出は翌年度にまわすこととしたため，結果的に次年度使用額が生じた。
前年度使用予定であった物品費と謝金の繰り越し分について，９月までに執行を行う予定である。
|
