Journal Article @Article Artikel in Fachzeitschrift
 Show entries of: this year (2019) | last year (2018) | two years ago (2017) | Notes URL
 Action: login to update Options: Goto entry point

 Author, Editor(s)
 BibTeX cite key*: DGNVV99

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

 Journal
 Journal Title*: Theoretical Computer Science Journal's URL: http://www.elsevier.nl/locate/tcs Download URL for the article: Language: English

 Publisher
 Publisher's Name: Elsevier Publisher's URL: http://www.elsevier.com Publisher's Address: Amsterdam, the Netherlands ISSN:

 Vol, No, pp, Date
 Volume*: 243 Number: 1/2 Publishing Date: July 2000 Pages*: 167-184 Number of VG Pages: Page Start: Page End: Sequence Number: DOI:

 Note: (LaTeX) 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. URL for the Abstract: Categories, Keywords: Rigid E-Unification, Finite Tree Automata, Logic with Equality HyperLinks / References / URLs: Copyright Message: Personal Comments: Download Access Level:

 Correlation
 MPG Unit: Max-Planck-Institut für Informatik MPG Subunit: Programming Logics Group Audience: experts only Appearance: MPII WWW Server, MPII FTP Server, MPG publications list, university publications list, working group publication list, Fachbeirat

BibTeX Entry:

@ARTICLE{DGNVV99,
AUTHOR = {Degtyarev, Anatoli and Gurevich, Yuri and Narendran, Paliath and Veanes, Margus and Voronkov, Andrei},
TITLE = {Decidability and Complexity of Simultaneous Rigid {E}-unification with One Variable and Related Results},
JOURNAL = {Theoretical Computer Science},
PUBLISHER = {Elsevier},
YEAR = {2000},
NUMBER = {1/2},
VOLUME = {243},
PAGES = {167--184},