| Project/Area Number |
08680362
|
|---|
| Research Category |
Grant-in-Aid for Scientific Research (C)
|
| Allocation Type | Single-year Grants |
|---|
| Section | 一般 |
|---|
| Research Field |
計算機科学
|
|---|
| Research Institution | MIE UNIVERSITY |
|---|
Principal Investigator |
OYAMAGUCHI Michio Mie Univ., Faculty of Engineering, Professor, 工学部, 教授 (50111828)
|
|---|
| Project Period (FY) |
1996 – 1998
|
| Project Status |
Completed (Fiscal Year 1998)
|
| Budget Amount *help |
¥1,700,000 (Direct Cost: ¥1,700,000)
Fiscal Year 1998: ¥500,000 (Direct Cost: ¥500,000)
Fiscal Year 1997: ¥600,000 (Direct Cost: ¥600,000)
Fiscal Year 1996: ¥600,000 (Direct Cost: ¥600,000)
|
|---|
| Keywords | Term Rewriting Systems / Church-Rosser / nonlinear TRS / completion procedure / unification / automatic theorem proving / weight-preserving / completion of extended critical pairs / Church-Rosser(合流性) / 左線形TRS / 合流性 / 強重なり性 / 深さ保存性 |
|---|
| Research Abstract |
Church-Rosser (CR) is a very important property of term rewriting systems (TRS). Many sufficient conditions for this property have been obtained so far. However, there have been several important problems concerning CR which remain open. In this research project we have first investigated some unsolved problems for CR of nonlinear and nonterminating TRS's. By introducing the notion of depth-preserving (and weight-preserving) and new proof techniques, we have obtained some sufficient conditions for CR which do not need the right-linearity condition of TRS's for the first time. And by developing these proof techniques we have succeeded in obtaining a sufficient condition for CR applicable to every class of extended overlapping(i.e., E-overlapping) TRSs. Moreover, using this sufficient condition, we have succeeded in giving anew completion procedure of extended critical pairs which is applicable to every TRS and never fails for the first time. These results enable us to implement an automatic theorem proving system fornonli near and nonterminating TRS's which is completely different from the systems for terminating TRS's proposed so far.
In this research project we have also investigated the famous long-standing open problems concerning CR of left-linear TRS's. By introducing the notion of strong monotonicity of reduction sequences, we have succeeded in obtaining a significant partial result breaking through the difficulty for the first time. Moreover, we have investigated the unification problem of TRS's which is one of the most fundamental problems. We have succeeded in obtaining the remarkable new result that unification is decidable for confluent right-ground TRS's. This result is very interesting as it shows that there exists a wide subclass of nonterminating TRS's with the decidable unification problem. And the proposed new proof technique will be useful to obtain further new results.
|
