| Outline of Annual Research Achievements |
本研究の当初想定していた具体的な研究項目は以下の通りであった. (1) 論理の組み合わせメカニズムの開発. (2) 拡張組み合わせ論理体系の構築. (3) 構築する論理をベースにした知識推論アルゴリズムの開発. これらに対して, 本研究では以下の結果を得た.
(1)と(2)に関しては, 埋め込み定理を用いた論理の組み合わせメカニズムおよびそれに基づいた複数の拡張論理を提案した. 埋め込み定理の考え方に基づいて, 矛盾許容論理, 時間論理などのいくつかを組み合わせた拡張論理を複数提案した. そして, それらに対してクリプケスタイルの意味論およびシーケント・自然演繹スタイルの証明体系を与えた. さらに, それら意味論や証明体系に対して, 完全性定理, カット除去定理などの定理を証明した. これら定理を証明するにあたって埋め込み定理を用いた新たな証明手法を開発した. 提案したこのような証明手法を用いることによって, 今まで証明することができなかった多くの拡張論理に対する上記基本定理を証明できるようになった.
(3)に関しては, 上記の提案した意味論を用いたモデル検査への応用を提案した. 具体的には, 本研究で提案した矛盾許容時間論理, 矛盾許容確率時間論理および階層演算子を持つ時間論理のモデル検査への応用を提案した. まず, これら拡張論理を用いたモデル検査アルゴリズムを提案した. これらアルゴリズムは埋め込み定理に基づいたトランスレーション関数を使用することにより得られた. そして, これらを使用することにより, 矛盾状態を許容する臨床推論および階層性を持つ推論を検証する方法を提案した. 以上の結果により, 今まで, 論理を用いて適切に扱うことができなかったような応用分野に対して, 提案した拡張論理およびそれらの意味論・証明体系を使用することの有用性を明らかにすることができた.
|
