The decidability problem for rigid E-unification: A new proof and extensions

Rigid E-unification is a restricted kind of unification modulo equational theories, or E-unification, that arises in equational theorem proving method. Roughly speaking, in rigid E-unification equations in E can only be instantiated once. The thesis consists of three major parts. In the first part, we study the restricted case of rigid E-unification where all terms appearing in the problem is ground. We redefine Kozen\u27s notion of reduced presentations for finitely presented algebras. It is shown that there exists a renaming mapping between any two reduced canonical ground term rewrite systems equivalent to a set of ground equations. The second part contains a new method for rigid E-unification. It has been conjectured that Kozen\u27s method for the ground E-unification can be extended to the rigid E-unification problem. Ground E-unification is a special case of rigid E-unification where E is a set of ground equations. Our method is similar to Kozen\u27s algebraic proof of NP-completeness of ground E-unification, and consists of two steps: A nondeterministic step during which an assignment from the set of variables to the set of terms appearing in the problem is guessed, and a checking step using a congruence closure method. An extension of rigid E-unification to AC symbols is presented in the third part. We define rigid restricted AC E-unification, where the equations contain AC function symbols but not in root position. We present a method for finding a complete set of rigid restricted AC E-unifiers. As a consequence, it is shown that this problem is decidable by extending the proof of Gallier et al. for rigid E-unification