研究課題
H18年度とH19年度に開発した種々の形式仕様と証明スコアの分析に基づき、帰納法と場合分けの方法を整理しつつ、(帰納法に基づく)推論と探索を融合した検証法を体系化し、「証明スコア作成ツール」を設計し一部開発した。ツールの設計と開発は、「人間と機械が各々の優れた能力を発揮しつつ協力して行う検証を支援する」という方針に従い、探索を支援する機能に焦点を絞って行った。すなわち、帰納法に基づく推論を用いる証明スコアの作成は人間が行い、探索を用いる検証をツール(システム、機械)が支援する、という方針を採用した。具体的には、これまでの研究で得られた、(1)帰納法と場合分けの適用法、(2)推論と探索を融合した検証法、に関する以下のような知見に基づきツールの設計と開発を行った。[A]帰納法を用いた推論に基づく検証は、帰納スキーマの選択、帰納命題(帰納法で証明すべき命題)や補題の特定、などの検証すべき問題に関する深い理解を必要とするので、人間が証明スコアを作成しつつ対話的に行うのが適当である。[B]探索は、すべての可能な場合を網羅的に検査することにより、場合分けを自動化する。探索による網羅的な場合分けはツール化しシステムに支援させるのが適当である。[C]抽象化(abstraction)などにより、命題の検証を網羅的な場合分けの探索に帰着させるためには、一般的には帰納法による推論が必要である。この部分は人間が証明スコアを作成しつつ対話的に行うのが適当である。
すべて 2008 その他
すべて 雑誌論文 (14件) (うち査読あり 14件) 備考 (1件)
IEICE Transactions 91-D(5)
ページ: 1492-1503
人工知能学会誌 23-4
ページ: 529-536
情報処理(情報処理学会学会誌) 49-5
ページ: 521-529
コンピュータソフトウェア(日本ソフトウェア科学会学会誌) 25-2
ページ: 1-13
ページ: 14-27
コンピュータソフトウェア(日本ソフトウェア科学会学会誌) 25-3
ページ: 69-80
コンピュータソフトウェア(日本ソフトウェア科学会学会誌) 25-4
ページ: 68-84
コンピュータソフトウェア(日本ソフトウェア科学会学会誌) 26-1
ページ: 71-83
ページ: 78-84
Proc. of 1st VSTTE, Springer LNCS 4171
ページ: 277-290
Proc. of IEEE/ACS Intl. Conference on Computer Systems and Applications
ページ: 652-660
Proceedings of the 8^<th>, International Conference on Computer and Information Technology (8^<th> CIT), IEEE Computer Society Press
ページ: 754-759
Proceedings of the 10th International Conference on Formal Engineering Methods (10th ICFEM), Springer LNCS 5256
ページ: 187-206
Proc. of 2nd International Conference on Theory and Practice of Electronic Governance (2008), ACM Press
ページ: 98-104
http://www.ldl.jaist.ac.jp/cafeobj
