Proceedings Article, Paper @InProceedings Beitrag in Tagungsband, Workshop

 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
 Editor(s): Nipkow, Tobias dblp
 BibTeX cite key*: DGNVV98a

 Title, Booktitle
 Title*: The Decidability of Simultaneous Rigid E-Unification with One Variable Booktitle*: Proceedings of the 9th International Conference on Rewriting Techniques and Applications (RTA-98)

 Event, URLs
 URL of the conference: http://www4.informatik.tu-muenchen.de/~rta98/ URL for downloading the paper: Event Address*: Tsukuba, Japan Language: English Event Date* (no longer used): March 30 - April 1, 1998 Organization: Event Start Date: 20 September 2019 Event End Date: 20 September 2019

 Publisher
 Name*: Springer URL: Address*: Berlin, Germany Type:

 Vol, No, Year, pp.
 Series: Lecture Notes in Computer Science
 Volume: 1379 Number: Month: March Pages: 181-195 Year*: 1998 VG Wort Pages: ISBN/ISSN: 3-540-64301-X Sequence Number: DOI:

 (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 $\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. Keywords: Finite Tree Automata, Intuitionistic Logic 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:

@INPROCEEDINGS{DGNVV98a,
AUTHOR = {Degtyarev, Anatoli and Gurevich, Yuri and Narendran, Paliath and Veanes, Margus and Voronkov, Andrei},
EDITOR = {Nipkow, Tobias},
TITLE = {The Decidability of Simultaneous Rigid {E}-Unification with One Variable},
BOOKTITLE = {Proceedings of the 9th International Conference on Rewriting Techniques and Applications (RTA-98)},
PUBLISHER = {Springer},
YEAR = {1998},
VOLUME = {1379},
PAGES = {181--195},
SERIES = {Lecture Notes in Computer Science},