| Budget Amount *help |
¥5,070,000 (Direct Cost: ¥3,900,000、Indirect Cost: ¥1,170,000)
Fiscal Year 2013: ¥1,300,000 (Direct Cost: ¥1,000,000、Indirect Cost: ¥300,000)
Fiscal Year 2012: ¥2,340,000 (Direct Cost: ¥1,800,000、Indirect Cost: ¥540,000)
Fiscal Year 2011: ¥1,430,000 (Direct Cost: ¥1,100,000、Indirect Cost: ¥330,000)
|
|---|
| 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.
|
