Decidability and Complexity of Simultaneous Rigid E-Unification with One Variable and Related Results

  • Anatoli Degtyarev ,
  • Yuri Gurevich ,
  • Paliath Narendran ,
  • ,
  • Andrei Voronkov

Theoretical Computer Science | , Vol 243(1-2): pp. 167-184

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.