2006 Fiscal Year Annual Research Report
| Project/Area Number |
17700164
|
|---|
| Research Institution | National Institute of Information and Communications Technology |
|---|
Principal Investigator |
兼岩 憲 独立行政法人情報通信研究機構, 第二研究部門知識創成コミュニケーション研究センター知識処理グループ, 研究員 (00342626)
|
|---|
| Keywords | 形式オントロジー / 矛盾要因 / 順序ソート論理 / 本質属性 |
|---|
| Research Abstract |
本年度では、前年度で検討した矛盾要因(論理的な矛盾とオントロジー的な矛盾)に基づいてオントロジー記述言語を形式的に設計した。具体的には,概念に関する知識表現のために,論理型言語の形式的な拡張を行った。その際,知識表現に便利な記述を許して表現力の高い言語を実現すると同時に,その知識表現から推論したり矛盾を検出したりするために形式的な意味論を与える。この意味論により、実際に概念知識や知識べ一スに矛盾を含まないかどうか、そしてどのような論理的な結論を導くことができるかを明らかにできる。
本年度のアカデミックな研究成果として,上記の知識表現の考察に基づき強い否定と古典論理の否定の2つの否定演算子を導入した古典一階述語論理の形式化が挙げられる。直観主義論理において提案された強い否定は、否定文を直接的に表すのに用いることができ、その意味論は2つの充足可能性関係を用いたクリプキ・モデルによって定義されている。しかしながら、その意味解釈や充足可能性は必ずしも知識表現における否定に合致しているとは言えない。特に〜を強い否定、「を古典論理の否定としたとき、〜「の形をした二重否定(構成的な二重否定と呼ぶ)が適切に特徴づけられていない。そこで構成的な二重否定に対する意味論を提案し、2種類の否定の組合わせによる構成的な意味を特徴づけた。また、提案した意味論と公理系により強い否定と構成的な二重否定に関する知識表現の例で推論が可能なことを示した。
|
