# Item

ITEM ACTIONSEXPORT

Released

Journal Article

#### Decidability and Complexity of Simultaneous Rigid E-unification with One Variable and Related Results

##### MPS-Authors

##### Locator

There are no locators available

##### Fulltext (public)

There are no public fulltexts available

##### Supplementary Material (public)

There is no public supplementary material available

##### Citation

Degtyarev, A., Gurevich, Y., Narendran, P., Veanes, M., & Voronkov, A. (2000).
Decidability and Complexity of Simultaneous Rigid E-unification with One Variable and Related Results.*
Theoretical Computer Science,* *243*(1/2), 167-184.

Cite as: http://hdl.handle.net/11858/00-001M-0000-000F-341B-9

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