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 99-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 Pcomplete.

PDF file

In  RTA'98

Publisher  Springer Verlag
All copyrights reserved by Springer 2007.

Details

Previous Versions

Anatoli Degtyarev, Yuri Gurevich, Paliath Narendran, Margus Veanes, and Andrei Voronkov. The decidability of simultaneous rigid E-unification with one variable, April 1997.