2018 Fiscal Year Annual Research Report
Discovery and proof of inductive theorems with multi-context reasoning systems for algebraic software
| Project/Area Number |
16K00090
|
|---|
| Research Institution | Hokkaido University |
|---|
Principal Investigator |
栗原 正仁 北海道大学, 情報科学研究科, 教授 (50133707)
|
|---|
| Project Period (FY) |
2016-04-01 – 2019-03-31
|
| Keywords | 帰納的定理自動証明 / 補題生成 / 項書換え系 / 書換え帰納法 / 多重文脈推論 |
|---|
| Outline of Annual Research Achievements |
文脈（計算開始から現時点までに行った選択の列）が互いに類似した非決定性並行プロセス間には，多くの場合，同一の計算・推論の処理が多数共通に存在する。本研究は，それらを共通に処理することによってシステム性能を飛躍的に高めることを狙った「多重文脈型推論」の基盤を開発するという全体構想の中で，(1) 補助定理を自動生成して帰納的定理の自動証明を行う多重文脈型推論システムを開発すること，及び(2)それを代数的ソフトウェアの正しさの検証に応用してその可用性を高めること，を目的としている。
平成29年度までには，補助定理を自動生成する手法（トップダウン的な手法，ボトムアップ的な手法）及びそれらを多重文脈型推論システムとして総合化するシステムの基本的骨組みを計画し，研究成果として，ボトムアップ的な手法と書換え帰納法の組合せによる補助定理自動生成手法を提案し，国際会議等において発表していた。
平成30年度は，もう１つの手法であるトップダウン的な手法として，発散鑑定法を拡張した新しい補助定理自動生成手法 Peripheral Sculpture を提案し，書換え帰納法と多重文脈型推論の組合せの枠組み Multi-context Postulateを開発してそれをシステムに組み込み，本研究が想定している応用分野である代数的ソフトウェア検証分野特有のものを含む標準問題群69問を用いてシステムの性能評価を行った結果，現行の多重文脈型推論システムではこれまで証明できなかった33問のうち新たに18問を自動的に証明できるようになった。この研究成果は電子情報通信学会論文誌の英文誌で公表されている。さらに本研究及びそれに関連する一連の研究の成果を一般的に総括し，国際会議において発表を行うことにより，この分野の研究者にアイデアの原理やその意義等について広く啓発を行った。
|
