2010 Fiscal Year Final Research Report
Combining Rippling and Rewriting Induction for Inductive Theorm Proving
| Project/Area Number |
20500002
|
|---|
| Research Category |
Grant-in-Aid for Scientific Research (C)
|
| Allocation Type | Single-year Grants |
|---|
| 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) |
2008 – 2010
|
| Keywords | 定理自動証明 / 書き換えシステム / リップリング / 書き換え帰納法 / 潜在帰納法 / 健全一般化法 / 発散鑑定法 / 合流性 |
|---|
| Research Abstract |
Our focus in this project is inductive theorem proving based on term rewriting systems. We are, in particular, interested in rewriting induction methods. We extended rewriting induction to enhance provability of non-orientable conjectures, and we implemented an inductive theorem prover based on our extension. Lemma discovery is an important aspect of inductive theorem proving and we generalized a sound generalization technique and gave sound divergence critic, which are useful when the rewriting induction is equipped with the disproving mechanism. We propose rewriting induction framework to incorporate different lemma generation methods. We also investigate automated confluence proving, as it is a necessary property to extend rewriting induction with the disproving mechanism. We gave new techniques to prove confluence and implemented a confluence prover.
|
