de.mpg.escidoc.pubman.appbase.FacesBean
English
 
Help Guide Privacy Policy Disclaimer Contact us
  Advanced SearchBrowse

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 (Ed.), 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.