de.mpg.escidoc.pubman.appbase.FacesBean
Deutsch
 
Hilfe Wegweiser Datenschutzhinweis Impressum Kontakt
  DetailsucheBrowse

Datensatz

DATENSATZ AKTIONENEXPORT

Freigegeben

Zeitschriftenartikel

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

MPG-Autoren
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;

Externe Ressourcen
Es sind keine Externen Ressourcen verfügbar
Volltexte (frei zugänglich)
Es sind keine frei zugänglichen Volltexte verfügbar
Ergänzendes Material (frei zugänglich)
Es sind keine frei zugänglichen Ergänzenden Materialien verfügbar
Zitation

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.


Zitierlink: http://hdl.handle.net/11858/00-001M-0000-000F-341B-9
Zusammenfassung
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.