| Budget Amount *help |
¥4,420,000 (Direct Cost: ¥3,400,000、Indirect Cost: ¥1,020,000)
Fiscal Year 2014: ¥1,170,000 (Direct Cost: ¥900,000、Indirect Cost: ¥270,000)
Fiscal Year 2013: ¥780,000 (Direct Cost: ¥600,000、Indirect Cost: ¥180,000)
Fiscal Year 2012: ¥1,170,000 (Direct Cost: ¥900,000、Indirect Cost: ¥270,000)
Fiscal Year 2011: ¥1,300,000 (Direct Cost: ¥1,000,000、Indirect Cost: ¥300,000)
|
|---|
| Outline of Final Research Achievements |
The aim of this study is expansion of the reasoning database for computer verification system Mizar. By formalizing various theories in mathematics, the automatic proof or the automatic reasoning will be realized in the future. This study is one of approaches for a realization of an artificial intelligence. The results of this research are mainly three areas which are measure theory, calculus and functional analysis. In the measure theory, we formalized a construction of the measure for a given set. In calculus, a definition of higher-order partial differential and some elementary theorems of an ordinary differential equation were formalized. In functional analysis, the L1 space and the conjugate space were formalized. We published 13 papers in the relevant Society.
|
