| Research Abstract |
研究目的 :
本研究の目的は, 部分構造論理を含む非古典論理の証明システムおよび意味論を構築し, 非古典論理の理論的基盤を構築・整備するとともに情報科学への応用に役立てることである, 非古典論理の具体例としては, 線形論理, 適切論理, BCK論理, 等の部分構造論理族および, 時間論理, 知識論理が挙げられる, 特に, 線形論理は並行計算や資源依存推論を厳密に扱うための枠組みとしてソフトウェア科学への応用上有用である. 時間論理は時間に依存する推論やモデル検査技術への基礎を与える.
研究方法 :
本研究では, まず拡張線形論理および拡張時間論理に対する各種証明システムおよび意味論を構築する. そしてそれらシステムと意味論の基本的性質であるカット除去定理, (強)正規化定理および完全性定理を証明する. 以上のような理論的結果を利用することにより, 知識ベースシステム, オントロジー記述言語, 並行・分散システム, プログラミング言語, 等の論理的形式化を実現することを意図している. 本年度は, 上記目的を達成するための基盤となる理論構築を中心に行った.
研究成果 :
パラコンシステント論理, 時間論理および部分構造論理に対する証明システムおよび意味論を構築した. それら証明システムと意味論に対して, 埋め込み定理, カット除去定理, 強正規化定理, 完全性定理を証明した. それら枠組みを使用して, マルチエージェントシステム, 資源推論システム, モデル検査技術等に対する論理的基礎を与えた. 特に, 提案した線形時間無限認識論理の拡張体系を使用して, 時間に依存する共有知識推論に対する厳密な論理的形式化を得た.
|
