| 研究概要 |
事例研究にもとづき,汎用的な帰納的と場合分けの手法を開発し,それに基づき「証明スコア作成支援ツール」を設計した。具体的には以下を行った。
[A]仕様記述と検証の事例の解析を継続,深化し,証明スコアの標準的な記述法を開発した。
[B]帰納法と場合分けの方法をより汎用し,それに対応する証明スコアの記述法を開発した。
[C]検索(search)に基づく検証法と帰納法に基づく検証法を融合した検証例題を開発し,証明スコアとして定式化した。
[D][A],[B],[C]の成果に基づき,証明スコアの作成においてシステムが支援できる事項を洗い出し,証明スコア作成支援ツールの設計を開始した。ッールの設計は,不完全な自動化を狙うのではなく,(1)人間の助けが必要な部分では「いかに人間に的確な判断をさせるか」に焦点を当て,(2)人間と機械が各々の優れた能力を発揮し協力して検証を遂行する,という方針に従い,会話型の使用形態を重視したものとした。
以上の設計に際しては,今までに開発した事例が設計したツールで困難無く扱えるかについて思考実験を行いツールの有効性を検討した。また,設計したツールを使うことで,問題のモデル化法や仕様スタイルにどのような変化が起こるかについても検討した。さらに,検索に基づく検証法と帰納法に基づく検証法の連携に付いては,検索を用いて証明した事実を帰納法による検証に利用する方法と,帰納法による検証の結果を利用して検索による検証をより高速化する方法などについても検討した。
|
