Journal Article
@Article
Artikel in Fachzeitschrift

Show entries of:

this year (2024) | last year (2023) | two years ago (2022) | Notes URL

Action:

login to update
Options:








Author, Editor(s)
Author(s):
Degtyarev, Anatoli
Gurevich, Yuri
Narendran, Paliath
Veanes, Margus
Voronkov, Andrei		dblp
dblp
dblp
dblp
dblp

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, Abstract, ©

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},
 ADDRESS = {Amsterdam, the Netherlands},
 MONTH = {July},
}

Entry last modified by Christine Kiesel, 03/12/2010
Show details for Edit History (please click the blue arrow to see the details)Edit History (please click the blue arrow to see the details)
Hide details for Edit History (please click the blue arrow to see the details)Edit History (please click the blue arrow to see the details)

Editor(s)
Margus Veanes		Created
04/22/1999 09:05:03 PM
Revisions
10.
9.
8.
7.
6.		Editor(s)
Christine Kiesel
Anja Becker
Uwe Brahm
Christine Kiesel
Christine Kiesel		Edit Dates
14.09.2001 03:27:30 PM
05.04.2001 15:17:39
04/04/2001 07:31:23 PM
15.03.2001 04:28:26 PM
13.03.2001 11:49:43