Construction of reasoning library for realization of computer verification system

2014 Fiscal Year Final Research Report

• 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
• 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.

Free Research Field

情報数理工学