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

术语重写系统(TRS)是对一组方程进行推理和重写(计算)的重要计算模型，广泛应用于定理自动证明和软件验证等领域，近年来受到了广泛的关注。然而，关于TRS的许多重要问题仍然是悬而未决的，在本研究项目中，我们首先研究了TRS的一些尚未解决的重要问题，这些问题可能是非终止的或非线性的。利用新的证明技术，我们成功地推广了前人的结果，并在非线性TRSS的基本决策问题上获得了新的结果，这些问题的充分条件到目前为止还不是很清楚。也就是说，我们已经证明了对于半构造子TRSS，即使我们假设这些TRSS是一元或线性的，几乎所有的问题都是不可判定的，但对于合流半构造子TRSS，可接合性、单词和统一问题是可判定的，尽管可达性问题仍然是不可判定的。我们还得到了保证可达性的充分条件。其次，我们指出了F.Jacqumard关于平坦TRSS的可达性和合流性的不可判定性的证明是不正确的，并成功地得到了这些不可判断性的修正的、简单得多的证明。这些都是对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.