Construction of reasoning library for realization of computer verification system
| Project/Area Number |
23500029
|
|---|
| Research Category |
Grant-in-Aid for Scientific Research (C)
|
| Allocation Type | Multi-year Fund |
|---|
| Section | 一般 |
|---|
| Research Field |
Fundamental theory of informatics
|
|---|
| Research Institution | Gifu National College of Technology (2012-2014)
Nagano National College of Technology (2011) |
|---|
Principal Investigator |
ENDOU Noboru 岐阜工業高等専門学校, その他部局等, 准教授 (30342497)
|
|---|
| Project Period (FY) |
2011-04-28 – 2015-03-31
|
| Project Status |
Completed (Fiscal Year 2014)
|
| 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)
|
|---|
| Keywords | 形式化数学 / 形式検証 / 証明検証システム / 数理論理学 |
|---|
| 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.
|
Report
(5 results)
Research Products
(13 results)
