部分構造論理とそのソフトウェア記述への応用

点击翻译按钮获取中文摘要

1.論理型プログラミング言語の基礎理論の構築。レゾリューション原理は論理プログラミング言語Prologの基本となる演繹システムであり、古典論理をベースにしたHerbrandの定理をその理論的根拠としている。本研究では、パラコンシステント論理のバリアントに対してレゾリューション原理を基にした演繹システムを構成した。これら論理およびレゾリューションシステムに対してHerbrandの定理、カット除去定理、完全性定理、(論理とレゾリューションとの間の)同等性定理を証明した。これら結果は従来の古典論理に対する結果の自然な拡張になっている。また、構成したシステムを使用することにより、ある種の無矛盾性を許容することが可能な知識ベースや医療データベースを実現できる。2.並行および分散システムの論理的形式化と検証。線形論理は並行計算系の記述や資源依存的推論の記述に適した枠組みとして知られており、リアクティブシステムの記述、論理型および関数型プログラミング言語の基礎理論として広く利用されている。本研究では線形論理の新たな拡張をいくつか導入した。提案した論理族は以下のような利点を持つ。(1)計算機資源(メモリ、CPUタイム、等)をより精密に記述できる。(2)時間、空間に依存した並行、分散システムを適切に記述できる。(3)情報モデルおよびペトリネットモデルに対する完全性が成立する。また、提案した論理族の主な応用として以下を示した。(1)ペトリネットシステムの記述。(2)ウイルスに感染した分散システムの分析。(3)電子マネーシステムの記述。(4)その他の応用(有限資源分析、医療データベースシステム、等)。