| Budget Amount *help |
¥4,420,000 (Direct Cost: ¥3,400,000、Indirect Cost: ¥1,020,000)
Fiscal Year 2020: ¥1,430,000 (Direct Cost: ¥1,100,000、Indirect Cost: ¥330,000)
Fiscal Year 2019: ¥1,430,000 (Direct Cost: ¥1,100,000、Indirect Cost: ¥330,000)
Fiscal Year 2018: ¥1,560,000 (Direct Cost: ¥1,200,000、Indirect Cost: ¥360,000)
|
|---|
| Outline of Final Research Achievements |
Term rewriting is a model of computation based on equational logic. The notion of inductive theorems of term rewriting systems expresses validity of equations from the programming perspective, and conditional term rewriting systems are a rewriting framework that suits to model functional programs, based on horn-clause logic. In this project, we give a rewriting induction framework to prove horn-clause inductive theorems over conditional term rewriting systems. We also give a method to prove ground confluence of oriented conditional term rewriting systems, as well as a critical pairs criterion for level-commutativity of oriented conditional term rewriting systems, etc.
|
