2001 Fiscal Year Final Research Report Summary
Inductive theorem proving method for program verification
| 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)
|
|---|
| Project Period (FY) |
1998 – 2001
|
| 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.
|
