Fundamental properties of rewriting systems and automated theorem proving

项重写系统（TRS）是一种重要的方程组推理和重写（计算）模型，近年来受到广泛关注，在自动定理证明和软件验证等领域有着广泛的应用。然而，许多重要的问题，TRS的，可能是非终止或非线性仍然开放。在本研究项目中，我们首先调查了一些未解决的问题，TRS的合流（CR），这可能是非终止的。使用新的证明技术，我们已经成功地扩展了以前的结果，并推广了以前的充分条件，以确保CR左线性TRS的。接下来，我们证明了存在满足以下条件（a）<$（c）的TRS的子类S。(a)存在一个变换过程，它取任意的TRS并在S中产生一个等价的TRS，（B）S是计算上通用的，和（c）一个充分条件，确保任何TRS在S中的CR，使我们能够构造一个完成过程。我们利用上述S类CR的充分条件构造了一个新的完备化过程，并建立了自动定理证明基于这个完成过程。我们已经实现了一个新的定理证明系统的基础上，这些结果，并证明了它的有用性。在本研究项目中，我们还研究了TRS的统一问题，这是最重要的问题之一。我们已经证明了合流右接地TRS的统一问题是可判定的。通过扩展这种证明技术，我们已经证明了，统一问题是可判定的合流简单的TRS的，但它已被证明是不可判定的合流一元TRS的。

Term rewriting systems (TRS) have received much attention in recent years, for they are an important computation model for reasoning and rewriting (computing) over a set of equations, and used in various applications such as automated theorem proving and software verification. However, many significant problems concerning TRS's which may be nonterminating or nonlinear remain open.In this research project we have first investigated some unsolved problems for confluence (CR) of TRS's which may be nonterminating. Using new proof techniques we have succeeded in extending the previous results and generalizing the previous sufficient conditions for ensuring CR of left-linear TRS's. Next, we have shown that there exists a subclass S of TRS's satisfying the following conditions (a)〜(c).(a) There exists a transformation procedure which takes an arbitrary TRS and produces an equivalent TRS in S,(b) S is computationally universal, and(c) a sufficient condition for ensuring CR of any TRS in S which enables us to construct a completion procedure can be obtained.Moreover, we have constructed a new completion procedure using the above sufficient condition for CR of the class S and established the theoretical foundation of automated theorem proving based on this completion procedure. We have implemented a new theorem proving system based on these results and proved its usefulness.In this research project we have also investigated the unification problem of TRS's which is one of the most important ones. We have shown that the unification problem for confluent right-ground TRS's is decidable. By extending this proof technique we have proven that the unification problem is decidable for confluent simple TRS's, but it has been shown to be undecidable for confluent monadic TRS's.