2011 Fiscal Year Annual Research Report
Project/Area Number |
20700015
|
Research Institution | Waseda University |
Principal Investigator |
上出 哲広 早稲田大学, 高等研究所, 研究員 (60332053)
|
Keywords | 時間論理 / パラコンシステント論理 / モデル検査 / Webオントロジー言語 |
Research Abstract |
[研究の目的および概要]: 本研究の目的は,部分構造論理を含む非古典論理のセマンティクスおよび証明システムを構築し,非古典論理の理論基盤を整備するとともに情報科学への応用に役立てることである.本年度の研究では,時間論理およびパラコンシステント論理に対する証明システムおよびセマンティクスを構築するとともに,それらの情報科学への応用を模索した.時間論理に関する研究では,ソフトウェア検証手法の一つであるモデル検査に関する基礎を与えた.パラコンシステント論理に関する研究では,Webオントロジー言語の基礎を与えるためのいくつかの拡張論理を提案し,それらの基本的性質を明らかにした. [時間論理に関する成果]: 従来の線形時間論理を,マルチエージェント間のインタラクションを扱うことができるように拡張した.そのような拡張の1つに対して、モデル検査アルゴリズムの存在(決定可能性)を証明した.また,従来の線形時間論理を,多次元空間を表現可能なように拡張し,完全性定理おとびカット除去定理を証明した.従来の線形時間論理の時間軸の範囲を有限に制限した時間論理を提案し,完全性定理,決定可能性,およびカット除去定理を証明した. [パラコンシステント論理に関する成果]: パラコンシステント論理と記述論理の両方の拡張となる,いくつかのパラコンシステント記述論理のセマンティクスを比較した.これらセマンティクスのいくつかは,Webオントロジー言語の基礎として使用されているものである.ここでは,それらセマンティクスの基本的な部分は本質的に同等であることを証明した.証明は,従来の埋め込み定理を修正・拡張することにより行われた.また,それら基本的なパラコンシステント記述論理に対して補間定理を証明した.
|
Research Products
(25 results)