Decidability and complexity of simultaneous rigid E-unification with one variable and related results

We show that simultaneous rigid E-unification, or SREU for short, is decida ble and in fact EXPTIME-complete in the case of one variable. This result i mplies that the For All*There Exists For All* fragment of intuitionistic lo gic with equality is decidable: Together with a previous result regarding t he undecidability of the There Exists There Exists-fragment, we obtain a co mplete classification of decidability of the prenex fragment of intuitionis tic logic with equality, in terms of the quantifier prefix. It is also prov ed 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 all ows 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 ca se. (C) 2000 Elsevier Science B.V. All rights reserved.