| Budget Amount *help |
¥4,550,000 (Direct Cost: ¥3,500,000、Indirect Cost: ¥1,050,000)
Fiscal Year 2015: ¥1,560,000 (Direct Cost: ¥1,200,000、Indirect Cost: ¥360,000)
Fiscal Year 2014: ¥1,560,000 (Direct Cost: ¥1,200,000、Indirect Cost: ¥360,000)
Fiscal Year 2013: ¥1,430,000 (Direct Cost: ¥1,100,000、Indirect Cost: ¥330,000)
|
|---|
| Outline of Final Research Achievements |
The theory of term rewriting systems is widely used in the fields of automated theorem provings and computation models. Although several automated confluence provers of term rewriting systems have been developed recently, little work is reported on applications of them. This research aims to develop automated program verification methods based on automated confluence provers for term rewriting systems. Concrete results include confluence proving based on persistency and type information, automated inductive theorem proving based on program transformations, sufficient criteria for confluent nominal rewriting systems, a sufficient condition for termination of the tree automata completion, automated ground confluence proving, abstract reduction systems on ordered monoid.
|
