AG 1, AG 2, AG 3, AG 4   Info

Expert Audience

-- Not specified --

Saarbrücken

Dieser Vortrag berichtet über neuste Ergebnisse von Plandowski [2] zur String-Unifikation, die zeigen, da3 die Lösbarkeit von Wortgleichungen in PSPACE ist.

String-Unifikation ist das Lösen von Wortgleichungen. Markov
fragte bereits Mitte der 50'iger, ob die String-Unifikiation
entscheidbar ist. Diese Frage wurde später unter anderem von
so bekannten Logikern wie Plotkin, Löb und Siekmann untersucht.
Aber erst 1977 fand Markovs Schüler Makanin [1] einen Algorithmus,
der die Entscheidbarkeit der Stringunifikation zeigt. Dieses Resultat
gehört heute zu den berühmtesten in der theoretischen Informatik.

Die Komplexität von Makanins Algorithmus war lange Zeit unklar -
der Algorithmus ist wegen seiner Komplexität nur schwer zu
verstehen - konnte aber nach näheren Untersuchungen auf
3-NEXPTIME (dreifach exponentiellen nicht-deterministischen
Zeitbedarf) datiert werden. Plandowski veröffentlichte 1999
einen sensationellen neuen Algorithmus, der in PSPACE
(polynomieller Speicherverbrauch) die Lösbarkeit von
Wortgleichungen berechnet [2].

Spezielle Vorkenntnisse im Bereich der Unifikations-Theorie
setze ich nicht voraus. Alle Interessenten sind herzlich
eingeladen.

Gru3, Tim

[1] Makanin(1977). Russische Veröffentlichung: The problem of
solvability of equations in a free semigroup. Mat. Sb.,
Vol. 103(145), Seite 147-233.
Englische Übersetzung in Math. U.S.S.R. Sb. Vol. 32.

[2] Plandowski(1999). Satisfiability of Word Equations with
Constants is in PSPACE. In Proceedings of Symposium on
Foundations of Computer Science (FOCS 1999), Seite 495-500.

Tim Priesnitz

--email hidden

passcode not visible

logged in users only