| 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 |
|
|---|
| Research Collaborator |
Sato Haruhiko
|
|---|
| Project Period (FY) |
2016-04-01 – 2019-03-31
|
| Project Status |
Completed (Fiscal Year 2018)
|
| Budget Amount *help |
¥4,810,000 (Direct Cost: ¥3,700,000、Indirect Cost: ¥1,110,000)
Fiscal Year 2018: ¥650,000 (Direct Cost: ¥500,000、Indirect Cost: ¥150,000)
Fiscal Year 2017: ¥3,510,000 (Direct Cost: ¥2,700,000、Indirect Cost: ¥810,000)
Fiscal Year 2016: ¥650,000 (Direct Cost: ¥500,000、Indirect Cost: ¥150,000)
|
|---|
| 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.
|
| Academic Significance and Societal Importance of the Research Achievements |
ソフトウェア工学の理論的基礎分野では，作成したソフトウェアの正しさを機械的に確認する技術が重要視されている。そのため代数的にソフトウェアの仕様を記述して実装する技術が考案されており，そこではソフトウェアの正しさを数学的な帰納的定理の証明に帰着させ，それを計算機により自動的に証明するアプローチを採っている。本研究成果はそのような技術開発に対して有益な知見を提供する点に学術的意義があるとともに，最終的にはソフトウェアの正しさの保証を通じて，安心・安全な情報社会の実現に寄与し得る点に社会的意義が認められる。
|
