Inductive theorem proving and its application with multi-context reasoning systems for algebraic software
| Project/Area Number |
25330074
|
|---|
| Research Category |
Grant-in-Aid for Scientific Research (C)
|
| Allocation Type | Multi-year Fund |
|---|
| Section | 一般 |
|---|
| Research Field |
Software
|
|---|
| Research Institution | Hokkaido University |
|---|
Principal Investigator |
|
|---|
| Co-Investigator(Renkei-kenkyūsha) |
SATO Haruhiko 北海道大学, 大学院情報科学研究科, 助教 (30543178)
|
|---|
| Research Collaborator |
JI ChengCheng
TAKAMATSU Hiroki
DING Rui
|
|---|
| Project Period (FY) |
2013-04-01 – 2016-03-31
|
| Project Status |
Completed (Fiscal Year 2015)
|
| Budget Amount *help |
¥5,070,000 (Direct Cost: ¥3,900,000、Indirect Cost: ¥1,170,000)
Fiscal Year 2015: ¥650,000 (Direct Cost: ¥500,000、Indirect Cost: ¥150,000)
Fiscal Year 2014: ¥3,770,000 (Direct Cost: ¥2,900,000、Indirect Cost: ¥870,000)
Fiscal Year 2013: ¥650,000 (Direct Cost: ¥500,000、Indirect Cost: ¥150,000)
|
|---|
| Keywords | 項書換え系 / 帰納的定理自動証明 / 多重文脈推論 / 代数的ソフトウェア / 代数的仕様記述 / システム形式検証 / 帰納的定理証明 / 多重文脈型推論 |
|---|
| Outline of Final Research Achievements |
Multi-context reasoning systems which execute termination verification, completion, and inductive theorem proving efficiently on parallel computers have been developed. Based on standard benchmark problems on the verification of correctness of algebraic software, it has been verified that the systems succeeded in the reasoning by finding more appropriate contexts than the previous systems and, by automatically generating useful lemmas, could solve the problems which had been unsolved before. By combining heuristics and artificial intelligence technology on searching, implementation techniques of automated termination verification on parallel computers have been developed. By using the lazy evaluation mechanism of the programming language SCALA, the efficiency of the execution of the systems has been improved.
|
Report
(4 results)
Research Products
(9 results)
