Share on Facebook Tweet on Twitter Share on LinkedIn Share by email
The decidability of simultaneous rigid E-unification with one variable

Anatoli Degtyarev, Yuri Gurevich, Paliath Narendran, Margus Veanes, and Andrei Voronkov

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

Details

Publication typeInproceedings
Published inRTA'98
Pages181-195
Volume1379
SeriesLNCS
PublisherSpringer Verlag

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.

> Publications > The decidability of simultaneous rigid E-unification with one variable