Toward a formal proofs and automated verifications of discrete mathematics
| Project/Area Number |
25610034
|
|---|
| Research Category |
Grant-in-Aid for Challenging Exploratory Research
|
| Allocation Type | Multi-year Fund |
|---|
| Research Field |
Foundations of mathematics/Applied mathematics
|
|---|
| Research Institution | Kyushu University |
|---|
Principal Investigator |
MIZOGUCHI Yoshihiro 九州大学, マス・フォア・インダストリ研究所, 准教授 (80209783)
|
|---|
| Project Period (FY) |
2013-04-01 – 2015-03-31
|
| Project Status |
Completed (Fiscal Year 2014)
|
| Budget Amount *help |
¥3,640,000 (Direct Cost: ¥2,800,000、Indirect Cost: ¥840,000)
Fiscal Year 2014: ¥1,820,000 (Direct Cost: ¥1,400,000、Indirect Cost: ¥420,000)
Fiscal Year 2013: ¥1,820,000 (Direct Cost: ¥1,400,000、Indirect Cost: ¥420,000)
|
|---|
| Keywords | 数理論理学 / 数学の形式化 / 検証可能証明 / ソフトウェア検証 / 離散数学 / 計算理論 / 形式証明 / 定理証明検証 / Coq / 証明支援系 / 定理証明器 / 有限オートマトン / Isabelle / Mizar |
|---|
| Outline of Final Research Achievements |
Our main results include a formalization of finite automata, sticker system and Fuzzy database as a formal specification of mathematics of discrete objects. A successful international workshop about "Theorem proving and provers for reliable theory and implementations" were held with over 80 participants including engineers in companies and researchers of computer science and mathematics. The famous unsolved problem for more than 400 years ago, Kepler conjecture was solved by Thomas Hales using formalized proofs last year. We publicized their result with introductions. Further, we appealed the importance and future view of the formalization of mathematics especially to students and teachers who are going to study mathematics in future.
|
Report
(3 results)
Research Products
(19 results)
