2003 Fiscal Year Annual Research Report
Project/Area Number |
03J09038
|
Research Institution | Keio University |
Principal Investigator |
上出 哲広 慶應義塾大学, 文学研究科, 特別研究員(PD)
|
Keywords | 部分構造論理 / 構成的否定 / 様相論理 / クリプキ意味論 / シーケント計算 / カット除去定理 / 完全性定理 |
Research Abstract |
1.構成的否定(または強い否定)を持つ命題部分構造論理族に対して、新たなクリプキ型の意味論およびシーケントスタイルの構文論を与え、完全性定理およびカット除去定理を証明することができた。 この結果により、多くの部分構造論理に対して、自然な「情報的解釈」を与えることができ、各々の論理に対する直感的意味がより明確になった。構成的否定結合子が表現している、論理式に対する「反証可能性解釈」が意味論的・構文論的に明らかになったため、従来知られていなかったような、論理間の対応関係を明らかにすることができた。構成的否定を持つ論理は論理プログラミング言語への応用において、不完全情報を許容するような大規模データベースを記述したり、非単調な推論を表現するために有用であることが知られている。本結果はそれら応用に対する適用範囲を資源性や並行性を考慮した分野へ拡張する可能性および、より記述力の高い部分構造論理をベースにした応用への可能性を示唆するものである。 2.上記の結果を、様々な様相記号を加えた部分にまで拡張することができた。 この結果により、様々な様相記号を持つ拡張多様相命題部分構造論理に対する理論的基礎を与えることができた。具体的には、「資源の消費関係」を表現する様相記号、「知識または信念」を表現する様相記号、そして「時間の経過」を表現する様相記号を持つ多くの応用上有用な部分構造論理を構成・特定することができ、それらに対して、完全性の成立する公理化という観点から厳密な理論的正当性を与えることができた。これら様相記号は、部分構造論理をベースにした、並行計算系、セキュリティープロトコル検証系および論理プログラミング言語系の表現能力を高めるために有用となるものである。
|
Research Products
(5 results)
-
[Publications] 上出哲広: "Normal modal substructural logics with strong negation"Journal of Philosophical Logic. 32. 589-612 (2003)
-
[Publications] 上出哲広: "A note on dual-intuitionistic logic"Mathematical Logic Quarterly. 49(5). 519-524 (2003)
-
[Publications] 上出哲広: "A simplified semantics for a fragment of intuitionistic linear logic"Bulletin of the Section of Logic. 32(3). 123-129 (2003)
-
[Publications] 上出哲広: "Quantized linear logic, involutive quantales and strong negation"Studia Logica. 受理済.
-
[Publications] 上出哲広: "Combining soft linear logic and spatio-temporal operators"Journal of Logic and Computation. 受理済.