| 研究概要 |
平成21年度は,平成20年度に行った研究、すなわち、「完備化」の推論システムを多重文脈型として設計・実装・評価を行う研究をさらに継続するとともに,その成果を「帰納的定理証明」へ応用し、標準的なテスト問題として知られる種々の定理を証明することに成功した。また、その成果を学術論文として投稿し、採択が決定された。具体的には,次のような研究を実施した。
(1)これまで停止性検証および完備化の推論システムを多重文脈型として設計した結果ならびにヒューリスティック探索の性能評価に関する研究成果に基づき,それらに対して共通の実行基盤を与えることのできるミドルウェアの設計・実装を完成させた。特に,等式を左右のいずれに向き付けるかの判断に依存じた文脈に焦点をしぼり,その多重文脈の表現と処理方法の設計結果を実装した。
(2)インスブルック大学(オーストリア)のチームと協働して、多重文脈型完備化システムの詳細な設計および実装を完成させた。上記のミドルウェアを適切に調整し,それを再利用可能とするようなプログラムの設計結果に基づいて実装し,ドキュメントを作成した。また,ベンチマークテストによりその有効性を評価した。
(3)上記の成果を等式における帰納的定理証明に応用し,手続きを設計・実装し,評価を行った。結果は良好であり、その成果を国際会議において発表したほか、電子情報通信学会英文論文誌「フォーマルアプローチ特集」に投稿し、採択決定された。
(4)今後の研究課題として、動的な並行システムのふるまいを取り扱うため、モデル検査との関連にっいて検討を行う第一歩として、モデル検査システムの入出力および制約に関する表現について検討を行った。モデル検査システムの入出力に関する検討内容は国際会議において発表した。制約に関しては、論文誌での採択が決定した。
|
