2008 Fiscal Year Annual Research Report
計算とルディクス:論理・計算・複雑さのための一般的フレームワーク構築に向けて
Project/Area Number |
08F08803
|
Research Institution | Kyoto University |
Principal Investigator |
照井 一成 Kyoto University, 数理解析研究所, 准教授
|
Co-Investigator(Kenkyū-buntansha) |
BASALDELLA Michele 京都大学, 数理解析研究所, 外国人特別研究員
|
Keywords | linear logic / ludics / completeness theorem |
Research Abstract |
本年度は以下の3点を目標としていた。 1.ルディクス理論を反復に関して拡張する問題に最終解決を与える。 2.計算論的ルディクスを拡張することにより、さまざまな論理学的現象にルディクスの観点から説明を与える。 3.余代数理論とルディクスの関係の確立 1については、予定通りにC.Faggian博士との共同研究を遂行し、ルディクスの基本定理たる充満完全性定理(統語論と意味論の完全対応)に完全な証明を与えることに成功した。成果は国際学会LICS'09に投稿し、受理された。 また雑誌論文の執筆をほぼ完了し、近日中に投稿予定である。 2については、ルディクスの枠組みで伝統論理学的なゲーデル完全性とゲーム意味論的な対話的完全性の間の関係を研究した。ゲーデル完全性は、どんな命題についても証明か反例モデルかのどちらか一方が存在することを主張するものであるが、そこには(現実のディベートに見られるような)証明と反例モデルの間の対話は見られない。 ゲーム意味論においては、証明と反証の間の対話を伴うより現実に即した形の完全性概念の萌芽がみられるが、明確であるとは言い難い。本研究は、ルディクスの枠組みで、対話的完全欧の概念をより明確にした。その上でゲーデル完全性を導くのと類似の手法(証明探索法)を用いて対話的完全性定理を証明した。結果としてゲーデル完全性のもつさまざまな性質(特にレーヴェンハイム=スコーレム定理)が対話的な文脈にもたらされることとなった。 成果は国際学会TLCA'09に投稿し、受理された。また4th NII Type Theory WorkshopおよびGames for Logic and Programming Languagesワークショップにおいて口頭発表を行った。 3については、研究を継続中である。
|
Research Products
(4 results)