hide
Free keywords:
-
Abstract:
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 A*EA*-fragment of intuitionistic logic with equality is
decidable. Together with a previous result regarding the undecidability of the
EE-fragment, we obtain {\em 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.
