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:




Library Locked Library locked




Author, Editor

Author(s):

Jez, Artur

dblp



Editor(s):

Esparza, Javier
Fraigniaud, Pierre
Husfeldt, Thore
Koutsoupia, Elias

dblp
dblp
dblp
dblp

Not MPII Editor(s):

Esparza, Javier
Fraigniaud, Pierre
Husfeldt, Thore
Koutsoupia, Elias

BibTeX cite key*:

Jez2014ICALP

Title, Booktitle

Title*:

Context Unification is in PSPACE

Booktitle*:

41st International Colloquium on Automata, Languages, and Programming (ICALP 2014)

Event, URLs

URL of the conference:

http://icalp2014.itu.dk/

URL for downloading the paper:


Event Address*:

Copenhagen, Denmark

Language:

English

Event Date*
(no longer used):


Organization:

European Association for Theoretical Computer Science (EATCS)

Event Start Date:

7 July 2014

Event End Date:

11 July 2014

Publisher

Name*:

Springer

URL:

http://www.springer.com

Address*:

Heidelberg

Type:

Extended abstract

Vol, No, Year, pp.

Series:

Lecture Notes in Computer Science

Volume:

8573

Number:


Month:

July

Pages:

244-255

Year*:

2014

VG Wort Pages:


ISBN/ISSN:


Sequence Number:


DOI:

10.1007/978-3-662-43951-7_21



Note, Abstract, ©


(LaTeX) Abstract:

Contexts are terms with one `hole', i.e. a place in which we can substitute an argument.
In context unification we are given an equation over terms with variables representing contexts
and ask about the satisfiability of this equation.
Context unification at the same time is subsumed by a second-order unification, which is undecidable,
and subsumes satisfiability of word equations, which is in PSPACE.
We show that context unification is in PSPACE, so as word equations.
For both problems NP is still the best known lower-bound.

This result is obtained by an extension of the recompression technique, recently developed by the author and used in particular
to obtain a new PSPACE algorithm for satisfiability of word equations, to context unification.
The recompression is based on applying simple compression rules (replacing pairs of neighbouring function symbols),
which are (conceptually) applied on the solution of the context equation and modifying the equation in a way so that such
compression steps can be performed directly on the equation, without the knowledge of the actual solution.

Keywords:

Context unification, Second order unification, Term rewriting



Download
Access Level:

Internal

Correlation

MPG Unit:

Max-Planck-Institut für Informatik



MPG Subunit:

Algorithms and Complexity Group

Audience:

experts only

Appearance:

MPII WWW Server, MPII FTP Server, MPG publications list, university publications list, working group publication list, Fachbeirat, VG Wort



BibTeX Entry:

@INPROCEEDINGS{Jez2014ICALP,
AUTHOR = {Jez, Artur},
EDITOR = {Esparza, Javier and Fraigniaud, Pierre and Husfeldt, Thore and Koutsoupia, Elias},
TITLE = {Context Unification is in PSPACE},
BOOKTITLE = {41st International Colloquium on Automata, Languages, and Programming (ICALP 2014)},
PUBLISHER = {Springer},
YEAR = {2014},
TYPE = {Extended abstract},
ORGANIZATION = {European Association for Theoretical Computer Science (EATCS)},
VOLUME = {8573},
PAGES = {244--255},
SERIES = {Lecture Notes in Computer Science},
ADDRESS = {Copenhagen, Denmark},
MONTH = {July},
DOI = {10.1007/978-3-662-43951-7_21},
}


Entry last modified by Artur Jez, 12/15/2014
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)
[Library]
Created
11/24/2014 02:13:54 PM
Revision
1.
0.


Editor
Artur Jez
Artur Jez


Edit Date
11/24/2014 04:34:32 PM
11/24/2014 02:13:54 PM