2013 Fiscal Year Final Research Report
Lemma Generation in Inductive Theorem Proving
| Project/Area Number |
23500002
|
|---|
| Research Category |
Grant-in-Aid for Scientific Research (C)
|
| Allocation Type | Multi-year Fund |
|---|
| Section | 一般 |
|---|
| Research Field |
Fundamental theory of informatics
|
|---|
| Research Institution | Tohoku University |
|---|
Principal Investigator |
AOTO takahito 東北大学, 電気通信研究所, 准教授 (00293390)
|
|---|
| Co-Investigator(Kenkyū-buntansha) |
TOYAMA Yoshihito 東北大学, 電気通信研究所, 教授 (00251968)
|
|---|
| Project Period (FY) |
2011 – 2013
|
| Keywords | 項書き換えシステム / 自動定理証明 / 帰納的定理 / 補題発見 |
|---|
| Research Abstract |
Our focus in this project is inductive theorem proving based on term rewriting systems. We are interested in identifying lemmas that leads the whole inductive theorem proving procedure to success. Our first attempt to this problem lies in how to extract information from divergence of proving procedure. For this, we investigated theories of unification and rewriting of regular terms and semi-unification that suits for expressing and detecting looping structures. We extended decision procedure for inductive theorems based on rewriting induction, and also we give a novel decision procedure of inductive theorems based on a new approach employing decision procedures for validity in initial algebras. We also studied how one can extract suitable properties from tail-recursive function definition for translating them to equivalent simple recursive one.
|
