We show that simultaneous rigid E-unification, or SREU for short, is decidable and in fact EXPTIME-complete in the case of one variable. This result implies that the ∀*∃∀* fragment of intuitionistic logic with equality is decidable. Together with a previous result regarding the undecidability of the 33-fragment, we obtain a complete classification of decidability of the prenex fragment of intuitionistic logic with equality, in terms of the quantifier prefix. It is also proved that SREU with one variable and a constant bound on the number of rigid equations is P-complete. Moreover, we consider a case of SREU where one allows several variables, but each rigid equation either contains one variable, or has a ground left-hand side and an equality between two variables as a right-hand side. We show that SREU is decidable also in this restricted case.

}, author = {Anatoli Degtyarev and Yuri Gurevich and Paliath Narendran and Margus Veanes and Andrei Voronkov}, journal = {Theoretical Computer Science}, number = {1-2}, pages = {167-184}, publisher = {Elsevier}, title = {Decidability and complexity of simultaneous rigid E-unification with one variable and related results}, url = {http://research.microsoft.com/apps/pubs/default.aspx?id=77840}, volume = {243}, year = {2000}, }