|
並列計算機上で多重文脈型推論基盤システムを開発し，停止性検証，完備化，帰納的定理証明を効率良く実行するシステムを開発した。代数的ソフトウェアの正しさの検証に関わる標準的なベンチマーク問題について，従前よりも文脈を適切に探索して推論に成功することと，従前のシステムでは解けなかった問題が，補助定理を自動生成することで解けることを確認した。
探索に関わる人工知能技術とヒューリスティクスを組み合わせることによって，本システムの重要部分である停止性自動検証の並列計算機上での実装技術を開発し，効率を向上させた。また，プログラミング言語SCALAのもつ遅延評価機構を用いて，システムの実行効率を改善した。
|
