Syntactic Duality of Classical Logic and Its Computational Aspect
Project/Area Number |
18700008
|
Research Category |
Grant-in-Aid for Young Scientists (B)
|
Allocation Type | Single-year Grants |
Research Field |
Fundamental theory of informatics
|
Research Institution | Kyoto University |
Principal Investigator |
NAKAZAWA Koji Kyoto University, 大学院・情報学研究科, 助教 (80362581)
|
Project Period (FY) |
2006 – 2008
|
Project Status |
Completed (Fiscal Year 2008)
|
Budget Amount *help |
¥2,510,000 (Direct Cost: ¥2,300,000、Indirect Cost: ¥210,000)
Fiscal Year 2008: ¥910,000 (Direct Cost: ¥700,000、Indirect Cost: ¥210,000)
Fiscal Year 2007: ¥700,000 (Direct Cost: ¥700,000)
Fiscal Year 2006: ¥900,000 (Direct Cost: ¥900,000)
|
Keywords | 古典論理 / シーケント計算 / カット除去 / 自然演繹 / カリーハワード同型 / 存在型 / 型検査 / 型推論 / 決定問題 / CPS変換 / 置換簡約 / 一般除去規則 / 自然演出繹 / 証明正規化 / 強正規化性 / 合流性 |
Research Abstract |
本研究では以下の結果を得た。(1) 直観主義シーケント計算のカット除去として、自然演繹の証明正規化と同型であるものを提案した。(2) 存在型を持つ型付きラムダ計算における型検査問題、型推論問題が決定不能であることを証明した。
|
Report
(4 results)
Research Products
(14 results)