| 研究課題/領域番号 |
25330013
|
|---|
| 研究種目 |
基盤研究(C)
|
| 配分区分 | 基金 |
|---|
| 応募区分 | 一般 |
|---|
| 研究分野 |
情報学基礎理論
|
|---|
| 研究機関 | 京都大学 |
|---|
研究代表者 |
照井 一成 京都大学, 数理解析研究所, 准教授 (70353422)
|
|---|
| 研究期間 (年度) |
2013-04-01 – 2019-03-31
|
| 研究課題ステータス |
完了 (2018年度)
|
| 配分額 *注記 |
4,030千円 (直接経費: 3,100千円、間接経費: 930千円)
2017年度: 780千円 (直接経費: 600千円、間接経費: 180千円)
2016年度: 780千円 (直接経費: 600千円、間接経費: 180千円)
2015年度: 780千円 (直接経費: 600千円、間接経費: 180千円)
2014年度: 780千円 (直接経費: 600千円、間接経費: 180千円)
2013年度: 910千円 (直接経費: 700千円、間接経費: 210千円)
|
|---|
| キーワード | 部分構造論理 / 代数的証明論 / MacNeille完備化 / 順序代数の稠密化 / ラムダ計算 / 共通型 / Ω規則 / 二階述語論理 / 線形論理 / 証明ネット / 抽象代数論理 / 橋渡し定理 / 不動点定理 / Lukasiewicz論理 / 素朴集合論 / 多相型ラムダ計算 / 完備化 / エルブランの定理 / 整合空間 / 計算可能解析 / 稠密化 / 正準拡大 |
|---|
| 研究成果の概要 |
第一に、非古典論理の研究における証明論的手法と代数的手法の融合を求め、代数的証明論のプログラムを推進した。結果として、順序代数の新しい完備化（超MacNeille完備化）や稠密化の手法が得られ、ファジー論理のいくつかの体系について、標準完全性定理の代数的証明を与えることに成功した。第二に、代数的・意味論的観点から関数型プログラミングの基礎研究（構成的証明論・ラムダ計算）を行った。特に、伝統的証明論におけるΩ規則の技法が順序代数におけるMacNeille完備化と密接に関係することを見出し、「論理のカット除去＝算術の１無矛盾性」という既知の対応を帰納的定義の諸体系へと敷衍した。
|
| 研究成果の学術的意義や社会的意義 |
「回り道を含む証明をまっすぐにすること」と「与えられた順序代数（ブール代数等）を完備化すること」の間には密接な関係がある。証明と代数の間に見られるこの種の対応関係をなるべく多く見出し、系統化すること、それにより伝統的に二分された証明論と（代数的）意味論の垣根を取り払い、両者の相乗効果で新しい成果を導き出すこと、それが本研究の目標であり存在意義である。また数学基礎論的な証明論（数学理論の「強さ」を調べる）とコンピュータ科学的な証明論（「証明＝プログラム」という観点から証明のダイナミズムを調べる）の垣根を取り払うことにもつながる。このように本研究は様々な理論やアプローチを「橋渡し」する意義を持つ。
|
