| 研究課題/領域番号 |
12780195
|
|---|
| 研究種目 |
奨励研究(A)
|
| 配分区分 | 補助金 |
|---|
| 研究分野 |
計算機科学
|
|---|
| 研究機関 | 群馬大学 (2001)
東京工業大学 (2000) |
|---|
研究代表者 |
吉浦 紀晃 群馬大学, 総合情報処理センター, 助教授 (00302969)
|
|---|
| 研究期間 (年度) |
2000 – 2001
|
| 研究課題ステータス |
完了 (2001年度)
|
| 配分額 *注記 |
1,800千円 (直接経費: 1,800千円)
2001年度: 1,400千円 (直接経費: 1,400千円)
2000年度: 400千円 (直接経費: 400千円)
|
|---|
| キーワード | 適切さの論理 / リアクティブシステム / 知識推論 / 決定可能性 / プログラム合成 / 形式的仕様記述 / 時間論理 / 段階的充足可能性 / 実現可能性 |
|---|
| 研究概要 |
本研究では、論理結合子の適切さという概念を用いて知識から有益な情報を推論することを目的として研究を行い、いくつかの成果を得た。第一に、古典論理における含意の違和感の除去を目的とした論理である適切さの論理の1つであるERのいくつかの性質を明らかにした。具体的には、従来の適切さの論理と同程度に違和感が除去されていること、決定可能であることを示した。また、modus ponenなど論理体系として満たすべき性質のいくつかが成り立たないことを明らかにし、この性質がなくともERは適切さの論理として十分な証明力を持つことを示した。
また、知識に基づいて有益な情報を推論するために、どのような論理結合子の適切さが必要であるかを考察するために、リアクティブシステムの仕様記述や検証を支援することを前提として、仕様記述や支援にとり有益な情報を導出するための論理体系の構築を行った。そのため、リアクティブシステムの仕様からプログラムを合成する方法や、仕様の性質を判定するための手続きを提案した。これらの方法を利用して、実際に、仕様の誤りがある場合に、どのような情報を提供すれば、仕様記述者にとって有効であり、それに基づいて仕様の訂正が行えるかについて考察した。
リアクティブシステムの仕様記述や検証に対する考察から、論理結合子の適切さを定義し、これに基づき、すべての論理結合子の適切さが導入された論理体系LRCを構築した。この論理体系に関する論文は、現在国際会議へ投稿中であり、今後、論文誌等を通じて成果を発表する予定である。
|
