研究課題/領域番号 |
21700014
|
研究種目 |
若手研究(B)
|
配分区分 | 補助金 |
研究分野 |
情報学基礎
|
研究機関 | 京都大学 |
研究代表者 |
照井 一成 京都大学, 数理解析研究所, 准教授 (70353422)
|
研究期間 (年度) |
2009 – 2012
|
研究課題ステータス |
完了 (2012年度)
|
配分額 *注記 |
4,160千円 (直接経費: 3,200千円、間接経費: 960千円)
2012年度: 910千円 (直接経費: 700千円、間接経費: 210千円)
2011年度: 910千円 (直接経費: 700千円、間接経費: 210千円)
2010年度: 1,170千円 (直接経費: 900千円、間接経費: 270千円)
2009年度: 1,170千円 (直接経費: 900千円、間接経費: 270千円)
|
キーワード | 数理論理学 / 線形論理 / 部分構造論理 / ルディクス / 再帰型 / エルブランの定理 / 代数的完備化 / ラムダ計算 / 計算量 / 共通型 / 情報基礎 / 線型論理 / 国際研究者交流 / オランダ:オーストリア:アメリカ / フランス:オーストリア:アメリカ:チェコ / フランス:オーストリア:アメリカ |
研究概要 |
(1) 代数的証明論の研究を部分構造論理の枠組みで推進した。部分構造論理の公理は階層性を成すことを示し、低い階層に属する論理について、カット除去定理と代数的な意味での完備化可能性が正確に対応することを示した。 (2) 線形論理から派生したゲーム意味論の一種であるルディクス理論を、余代数的・計算論的観点から再定式化した。構成的古典命題論理に相当する証明体系について対話的完全性定理を証明し、(プログラミング言語型理論の意味での)一般再帰型の解釈に応用した。
|