The Decidability of Simultaneous Rigid E-Unification with One Variable

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

• Type: Conference
• Year: 1998
• Where: RTA
• Authors: Anatoli Degtyarev, Yuri Gurevich, Paliath Narendran, Margus Veanes, Andrei Voronkov
• Keywords: Intuitionistic Logic, Prenex Fragment, RTA 1998, Simultaneous Rigid E-unification, Theoretical Computer Science