Improvement of lemma generation and reasoning strategies for automated inductive theorem proving
| Project/Area Number |
16K16032
|
|---|
| Research Category |
Grant-in-Aid for Young Scientists (B)
|
| Allocation Type | Multi-year Fund |
|---|
| Research Field |
Software
|
|---|
| Research Institution | Hokkai-Gakuen University |
|---|
Principal Investigator |
SATO HARUHIKO 北海学園大学, 工学部, 准教授 (30543178)
|
|---|
| Project Period (FY) |
2016-04-01 – 2018-03-31
|
| Project Status |
Completed (Fiscal Year 2017)
|
| Budget Amount *help |
¥1,300,000 (Direct Cost: ¥1,000,000、Indirect Cost: ¥300,000)
Fiscal Year 2017: ¥650,000 (Direct Cost: ¥500,000、Indirect Cost: ¥150,000)
Fiscal Year 2016: ¥650,000 (Direct Cost: ¥500,000、Indirect Cost: ¥150,000)
|
|---|
| Keywords | 定理自動証明 / 帰納的定理証明 / 補題自動生成 / 書き換え帰納法 / 項書換え系 / 形式的検証 |
|---|
| Outline of Final Research Achievements |
With the increasing importance of software systems, the need to ensure safety or correctness of them in a rigorous way is growing. Formal verification is a generic name of such a rigorous approach, where the meaning of the description of a system and of the desirable properties for the system are formalized unambiguously and we mathematically prove that the system has the properties under the formalization. For difficult proof tasks, human experts need to make proofs by hand. Since the cost for involving human experts is expensive, the improvement of automated theorem provers is one of the most important subjects for popularization of formal verification. In order to automate the proof of the type of theorems called inductive theorems, which is the class of theorems requiring mathematical (well-founded) induction to prove and hence is known to be hard to automate, in this study we propose new methods for automated lemma generation required for inductive theorem proving.
|
Report
(3 results)
Research Products
(2 results)
