Datensatz

Zusammenfassung

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 $\forall^*\exists\forall^*$ fragment of intuitionistic logic with equality is decidable. Together with a previous result regarding the undecidability of the $\exists\exists$-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.