Fundamental properties of rewriting systems and completion procedures

点击翻译按钮获取中文摘要

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.