权益分类	功能权益	普通用户	{{item.name}}会员
{{category.name}}	{{benefitItem.name}}

Fundamental properties of rewriting systems and completion procedures

重写系统和完成程序的基本属性

基本信息

批准号：
08680362
负责人：
OYAMAGUCHI Michio
金额：
$ 1.09万
依托单位：
MIE UNIVERSITY
依托单位国家：
日本
项目类别：
Grant-in-Aid for Scientific Research (C)
财政年份：
1996
资助国家：
日本
起止时间：
1996 至 1998
项目状态：
已结题

项目摘要

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.

Checking-Rosser(CR)是术语重写系统(TRS)的一个重要性质。到目前为止，人们已经得到了这一性质的许多充分条件。然而，与CR有关的几个重要问题仍然悬而未决。在这个研究项目中，我们首先研究了非线性非终止TRS的CR的一些未解决的问题，通过引入保深度(和保权)的概念和新的证明技巧，我们首次得到了CR不需要TRS的右线性条件的一些充分条件。通过发展这些证明技术，我们成功地得到了CR适用于每一类扩展重叠(即E-重叠)TRSS的充分条件。此外，利用这一充分条件，我们成功地给出了一种新的扩展临界对的完成过程，该过程适用于每一个TRS，且不会第一次失败。这些结果使我们能够实现一个与目前提出的终止TRS的系统完全不同的关于非线性近终止TRS的自动定理证明系统。在这个研究项目中，我们还研究了关于左线性TRS的CR的著名的长期未解决的问题。通过引入约简序列的强单调性的概念，我们首次成功地获得了一个有意义的部分结果。此外，我们还研究了TRS的统一问题，这是最基本的问题之一。我们成功地得到了合流右基TRS的合一是可判定的这一显著的新结果，这一结果非常有趣，因为它表明存在一个广泛的子类，即具有可判定合一问题的非终止TRS。所提出的新的证明方法将有助于进一步获得新的结果。