2004 Fiscal Year Annual Research Report
Project/Area Number |
03J09038
|
Research Institution | Keio University |
Principal Investigator |
上出 哲広 慶應義塾大学, 文学研究科, 特別研究員(PD)
|
Keywords | 線形論理 / 並行計算 |
Research Abstract |
1.並行性および資源性を適切に表現可能な拡張論理体系の構築。 Lafontにより導入されたソフト線形論理を拡張した。さらに、この拡張論理に対してKripke型のセマンティクスを与え、完全性定理を証明した。提案した論理は、資源性を表現することが可能な二種類の様相オペレータおよび新たに導入した時間・空間オペレータを持つ。これら様相オペレータを組み合わせることにより、並行計算や分散システム環境における時間・空間に依存した様々な状況を適切に表現できるようになった。完全性が成立するKripke型セマンティクスのカノニカルモデルを使用することによって、提案した論理に対する直感的に自然な情報的解釈を与えることができた。 2.並行計算および分散システムの論理的形式化および検証。 上記論理の並行計算および分散システムへの応用として、以下の事柄を示した。 (1)提案した論理に対するPetriネットによる並行計算的解釈を与えた。このことにより、この論理を使用することによる、並行計算系の分析・検証が可能になった。 (2)提案した論理を使用することにより、時間・空間に依存する分散システム環境におけるある種のセキュリティー問題を論理的に形式化した。このことにより、この問題の厳密な解決をはかることができた。 3.論理プログラミング言語の基礎付けを与える拡張論理体系の構築。 上記論理とは別に、古典論理の自然な拡張としていくつかの新たな論理体系を構築し、それらに対して完全性定理およびカット除去定理を証明した。これら論理族は構成的否定と呼ばれる否定結合子を持つ。この否定結合子は、これら論理をベースにした論理プログラミング言語を構成した場合、否定の扱いにおいてある種の無矛盾性を許容可能にする性質を持つ。
|
Research Products
(6 results)