Discovery and proof of inductive theorems with multi-context reasoning systems for algebraic software

2018 Fiscal Year Final Research Report

• Project/Area Number: 16K00090
• Research Category: Grant-in-Aid for Scientific Research (C)
• Allocation Type: Multi-year Fund
• Section: 一般
• Research Field: Software
• Research Institution: Hokkaido University
• Principal Investigator: Kurihara Masahito 北海道大学, 情報科学研究科, 教授 (50133707)
• Research Collaborator: Sato Haruhiko
• Project Period (FY): 2016-04-01 – 2019-03-31
• Keywords: 帰納的定理 / 定理自動証明 / 定理自動発見 / 補題生成 / 多重文脈型推論 / 代数的ソフトウェア / 項書換え系

Outline of Final Research Achievements

This research project uses new ideas of system structure called the multi-context reasoning system to apply them to the grand plan to develop technologies for automatic, efficient discovery and proof of a kind of mathematical theorems called inductive theorems, which play important roles in computer science and technology. To attain this purpose, we have developed software systems with new top-down and bottom-up methods for automatic generation of lemmas required in the proof of the main theorems. In addition, we have empirically shown the applicability of this technology in the field of the verification of correctness of algebraic software in software engineering.

Free Research Field

ソフトウェア科学

Academic Significance and Societal Importance of the Research Achievements

ソフトウェア工学の理論的基礎分野では，作成したソフトウェアの正しさを機械的に確認する技術が重要視されている。そのため代数的にソフトウェアの仕様を記述して実装する技術が考案されており，そこではソフトウェアの正しさを数学的な帰納的定理の証明に帰着させ，それを計算機により自動的に証明するアプローチを採っている。本研究成果はそのような技術開発に対して有益な知見を提供する点に学術的意義があるとともに，最終的にはソフトウェアの正しさの保証を通じて，安心・安全な情報社会の実現に寄与し得る点に社会的意義が認められる。