Fundamental properties of rewriting systems and automated theorem proving

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

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.