| Project/Area Number |
10680346
|
|---|
| Research Category |
Grant-in-Aid for Scientific Research (C)
|
| Allocation Type | Single-year Grants |
|---|
| Section | 一般 |
|---|
| Research Field |
計算機科学
|
|---|
| Research Institution | Tohoku University (2000-2001)
Japan Advanced Institute of Science and Technology (1998-1999) |
|---|
Principal Investigator |
TOYAMA Yoshihiro Research Institute of Electrical Communication, Tohoku University, Professor, 電気通信研究所, 教授 (00251968)
|
|---|
| Co-Investigator(Kenkyū-buntansha) |
KUSAKARI Keichirou Research Institute of Electrical Communication, Tohoku University, Resarch Asspcoate, 電気通信研究所, 助手 (90323112)
鈴木 大郎 東北大学, 電気通信研究所, 助手 (90272179)
|
|---|
| Project Period (FY) |
1998 – 2001
|
| Project Status |
Completed (Fiscal Year 2001)
|
| Budget Amount *help |
¥1,800,000 (Direct Cost: ¥1,800,000)
Fiscal Year 2001: ¥500,000 (Direct Cost: ¥500,000)
Fiscal Year 2000: ¥500,000 (Direct Cost: ¥500,000)
Fiscal Year 1999: ¥400,000 (Direct Cost: ¥400,000)
Fiscal Year 1998: ¥400,000 (Direct Cost: ¥400,000)
|
|---|
| Keywords | inductionless induction / rewriting induction / coverset induction / higher order / rewriting system / completion / 項書き換えシステム / 自動証明 |
|---|
| Research Abstract |
To propose a new theoretical basis of automated program verification, we have studied rewriting methods among the inductionless induction method, the rewriting induction method, the coverset induction method, and related methods used in automated thorem proving. Through theoretical analysis and experiments, we have obtained the following results:
(1) We analyzed the relation between the inductionless induction method and the rewriting induction method. It was shown that the main difference between two methods is that the inductionless induction method is based on the Church-Rosser property but the rewriting induction method is based on the strong normalization property. We also proved that the coverset induction can be naturally explained by the concept of rewriting induction.
(2) We developed several techniques for proving the termination property of term rewriting systems, AC term rewriting systems, and higher-order rewriting systems. New techniques proposed are tree lifting ordering, improved recursive decomposition ordering, higher-order simplification ordering, argument filtering transformation, and AC-dependent pair.
(3) We proposed a new conditional linearization based on left-right separated conditional term rewriting systems. By developing a concept of weight decreasing joinability we presented a sufficient condition for the Church-Rosser property of left-right separated conditional term rewriting systems.
|
