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:








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