Research in fundamental properties of rewriting systems and advanced theorem proving systems

项重写系统（TRS）是一种重要的方程组推理和重写（计算）模型，近年来受到广泛关注，在自动定理证明和软件验证等领域有着广泛的应用。然而，许多重要的问题，TRS的，可能是非终止或非线性仍然开放。在本研究项目中，我们首先调查了一些尚未解决的重要问题，TRS的，可能是非终止或非线性。使用新的证明技术，我们已经成功地扩展了以前的结果，并获得了新的结果的基本决策问题的非右线性TRS的充分条件，确保可判定性迄今为止还不知道。也就是说，我们已经表明，对于类的半构造TRS，几乎所有的问题仍然是不可判定的，即使我们假设这些TRS是一元或线性的，但可连接性，字和统一的问题是可判定的合流半构造TRS，虽然可达性问题仍然是不可判定的。我们也得到了保证可达性的判定性的充分条件。接下来，我们指出了F.Jacqumard给出的平坦TRS的可达性和汇流性的不可判定性的证明是不正确的，并成功地获得了这些不可判定性的修复和明显更简单的证明。这些都是否定的答案所提出的公开问题G.Godoy等人。在这个研究项目有关自动定理证明，我们已经建立了理论基础，这是基于最终的代数方法和适用于方程的高阶函数符号。我们已经实现了一个先进的定理证明系统的基础上，这一理论和我们的研究成果，其有用性已被证明的应用程序的密码协议验证。

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 important problems for TRS's which may be nonterminating or nonlinear. Using new proof techniques we have succeeded in extending the previous results and obtaining new results on fundamental decision problems for non-right-linear TRSs of which sufficient conditions ensuring the decidability have not been known so far. That is, we have shown that for the class of semi-constructor TRSs, almost all problems remain undecidable even if we assume that these TRSs are monadic or linear, but the joinability, word and unification problems are decidable for confluent semi-constructor TRSs, although the reachability problem remains undecidable. We have also obtained sufficient conditions for ensuring the decidability of reachability. Next, we have pointed out that the proofs of undecidability of reachability and confluence for flat TRSs given by F.Jacqumard are incorrect and succeeded in obtaining repaired and significantly simpler proofs of these undecidability. These are negative answers to the open problems posed by G.Godoy et al.In this research project concerning automate theorem proving, we has established the theoretical foundation which is based on the final algebra approach and applicable to equations with higher-order function symbols. We have implemented an advanced theorem proving system based on this thory and our research results whose usefulness has been proven by applications to cryptographic protocol verification.