2004 Fiscal Year Annual Research Report
ダイナミックに変化する知識・信念の論理学的分析手法の研究
| Project/Area Number |
04J07439
|
|---|
| Research Institution | Keio University |
|---|
Principal Investigator |
長谷部 浩二 慶應義塾大学, 文学部, 特別研究員(PD)
|
|---|
| Keywords | 知識論理 / Compositional losic / 認証プロトコル / 完全性定理 / 証明検索法 / 反例導出 |
|---|
| Research Abstract |
本年度は主に、ダイナミックな変化を伴う状況に関する論理推論を取り扱うための基本的枠組となる論理体系の構築を行った。特に認証プロトコルの安全性検証を例にとり、John Mitchellらの研究グループにより提案されたCompositional Logicの枠組をもとにした論理体系を考案した。本年度の前半では、Compositional Logicの枠組を単純化することにより、証明の融合を論理推論のレベルで行うことができることを示した。また本年度の後半では、認証プロトコルの安全性証明を、等式を伴う1階述語論理のみによって行う体系を考案した。その基本的なアイデアは、原子述語記号として基本的なアクションをとり、アクションの列をこれらの列として組み合わせた原子論理式で表現するというものである。これにより、従来の通常の1階述語論理で与えられてきたタルスキ的な意味論に「アクションの列」の概念を導入した自然な意味論を与えることができ、完全性定理の成り立つことを示すことができた。さらに、証明検索法による証明可能性判定が有限の手続きにより決定可能であることも示した。このような定理の成り立つ最大の利点は、これらの定理の応用として証明検索法による反例導出を1階述語論理の枠組の中で自然に行えるという点である。現在は、神戸大工学部の田村直之教授グループらとの共同研究として、定理証明系によるアルゴリズム試作実装を行なっている。また、上記で得られた枠組に、本年度前半で行ったcompositionalityや(量的時間制約を伴う)時間概念、さらに本研究の主要テーマである知識・信念の概念の導入を試み、より一般的な対象(例えば実時間システムやこれまで提起されてきた知識・信念に関わる状況など)の分析へと拡張することを目指している。
|
