Automated theorem proving methods in classical logic with equality that are based onthe Herbrand theorem, reduce to a problem called Simultaneous Rigid E-Unification,or SREU for short, Recent developments show that SREU has also close connectionswith intuitionistic logic with equality, second-order unification, some combinatorialproblems and finite tree automata.

We show new decidability results of various cases of SREU. In particular, we improve upon the undecidability result of SREU by showing its undecidability in a very restricted case, in fact the minimal known case. We prove the decidability of some casesof SREU under certain restrictions regarding the number of variables and other syntactical criteria, To prove the (computational) complexity of some cases, we reducethem to certain decision problems of finite tree automata, The complexity of the latterproblems is studied first. In connection with that, we present a survey of closely relatedproblems and give a comparison with the corresponding results in classical automatatheory.

These results are applied in the context of intuitionistic logic with equality, to obtaina complete classification of its prenex fragment in terms of the quantifier prefix: the ∃∃-fragment is shown undecdable and the ∀*∃∀*-fragment is shown decidable. These results have further implications for proof search in intuitionistic logic with equality.

We also improve upon a number of other recent undecidability results that are relatedto the so-called Herbrand Skeleton problem and are of fundamental importance inautomated theorem proving in in classical logic with equality. In that context we alsoprove, as our main tool, a logical theorem that we believe is of independent interest.