Decidability and Complexity of Simultaneous Rigid E-Unification with One Variable and Related Results - Degtyarev, Anatoli; Gurevich, Yuri; Narendran, Paliath; Veanes, Margus; Voronkov, Andrei (Theoretical Computer Science, 2000)
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. The journal version of [127a] containing also a decidability proof for the case of simultaneous rigid E-unification when each rigid equation either contains (at most) one variable or else has a ground left-hand side and the right-hand side of the form x=y where x and y are variables.