| Project/Area Number |
25330013
|
|---|
| Research Category |
Grant-in-Aid for Scientific Research (C)
|
| Allocation Type | Multi-year Fund |
|---|
| Section | 一般 |
|---|
| Research Field |
Theory of informatics
|
|---|
| Research Institution | Kyoto University |
|---|
Principal Investigator |
|
|---|
| Project Period (FY) |
2013-04-01 – 2019-03-31
|
| Project Status |
Completed (Fiscal Year 2018)
|
| Budget Amount *help |
¥4,030,000 (Direct Cost: ¥3,100,000、Indirect Cost: ¥930,000)
Fiscal Year 2017: ¥780,000 (Direct Cost: ¥600,000、Indirect Cost: ¥180,000)
Fiscal Year 2016: ¥780,000 (Direct Cost: ¥600,000、Indirect Cost: ¥180,000)
Fiscal Year 2015: ¥780,000 (Direct Cost: ¥600,000、Indirect Cost: ¥180,000)
Fiscal Year 2014: ¥780,000 (Direct Cost: ¥600,000、Indirect Cost: ¥180,000)
Fiscal Year 2013: ¥910,000 (Direct Cost: ¥700,000、Indirect Cost: ¥210,000)
|
|---|
| Keywords | 部分構造論理 / 代数的証明論 / MacNeille完備化 / 順序代数の稠密化 / ラムダ計算 / 共通型 / Ω規則 / 二階述語論理 / 線形論理 / 証明ネット / 抽象代数論理 / 橋渡し定理 / 不動点定理 / Lukasiewicz論理 / 素朴集合論 / 多相型ラムダ計算 / 完備化 / エルブランの定理 / 整合空間 / 計算可能解析 / 稠密化 / 正準拡大 |
|---|
| Outline of Final Research Achievements |
First, we have developed a research program called the algebraic proof theory, aiming at an integration of proof theoretic and algebraic methods in nonclassical logics. It has resulted in a new completion method for ordered algebras (hyper-MacNeille completion) and a method for densification, leading to a purely algebraic proof to the standard completeness of various fuzzy logics. Second, we have studied the foundations of functional programming (constructive proof theory and lambda calculus) from the algebraic-semantic point of view. In particular, we have focused on the Omega-rule technique in the traditional proof theory and discovered an intimate connection with
the MacNeille completion in ordered algebras. It has resulted in a generalization of the known correspondence between cut elimination in logic and 1-consistency in arithmetic to arithmetical theories of inductive definitions.
|
| Academic Significance and Societal Importance of the Research Achievements |
「回り道を含む証明をまっすぐにすること」と「与えられた順序代数（ブール代数等）を完備化すること」の間には密接な関係がある。証明と代数の間に見られるこの種の対応関係をなるべく多く見出し、系統化すること、それにより伝統的に二分された証明論と（代数的）意味論の垣根を取り払い、両者の相乗効果で新しい成果を導き出すこと、それが本研究の目標であり存在意義である。また数学基礎論的な証明論（数学理論の「強さ」を調べる）とコンピュータ科学的な証明論（「証明＝プログラム」という観点から証明のダイナミズムを調べる）の垣根を取り払うことにもつながる。このように本研究は様々な理論やアプローチを「橋渡し」する意義を持つ。
|
