de.mpg.escidoc.pubman.appbase.FacesBean
English

Help Guide Privacy Policy Disclaimer Contact us

# Item

ITEM ACTIONSEXPORT

Released

Conference Paper

#### The Decidability of Simultaneous Rigid E-Unification with One Variable

##### MPS-Authors
http://pubman.mpdl.mpg.de/cone/persons/resource/persons45106

Narendran,  Paliath
Programming Logics, MPI for Informatics, Max Planck Society;

http://pubman.mpdl.mpg.de/cone/persons/resource/persons45662

Veanes,  Margus
Programming Logics, MPI for Informatics, Max Planck Society;

http://pubman.mpdl.mpg.de/cone/persons/resource/persons45678

Voronkov,  Andrei
Programming Logics, MPI for Informatics, Max Planck Society;

##### 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. (1998). The Decidability of Simultaneous Rigid E-Unification with One Variable. In T. Nipkow (), Proceedings of the 9th International Conference on Rewriting Techniques and Applications (RTA-98) (pp. 181-195). Berlin, Germany: Springer.

Cite as: http://hdl.handle.net/11858/00-001M-0000-000F-389C-B
##### 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 $\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.