Ehrenfeucht-Fraïssé-Spiel

Aus Wikiludia
Wechseln zu: Navigation, Suche

Inhaltsverzeichnis

Ehrenfeucht-Fraïssé-Spiel

Bei diesem Spiel treffen die Bereiche der Spieltheorie, Automatentheorie und Logik zusammen.

Spielregeln

Beim Ehrenfeucht-Fraïssé-Spiel einigen sich die beiden Spieler S und D auf zwei Wörter u, v und eine festgelegte Zahl k von Runden.

(Der Begriff Wort wird hier wie in den Formalen Sprachen verwendet)

Die beiden Wörter werden untereinander geschrieben, so dass die Buchstaben mit Linien verbunden werden können.

Gezogen wird abwechselnd nach folgenden Regeln:
Spieler S (Spoiler) wählt aus einem der beiden Wörter einen bisher unbenutzten Buchstaben aus.
Spieler D (Duplicator) wählt aus dem anderen Wort den gleichen, unbenutzten Buchstaben aus.
Die beiden Buchstaben werden miteinander durch eine gerade Linie verbunden.

Gewonnen hat Spieler S, wenn Spieler D keinen passenden unbenutzten Buchstaben mehr auswählen kann, oder wenn die neue Linie eine bestehende Linie kreuzt.
Spieler D hat gewonnen, wenn nach den vereinbarten k Runden das Spiel noch nicht vorbei ist.

Beispiel:

Nehmen wir an, die Spieler haben sich auf die Worte "aababba" und "ababbaba" geeinigt und die Zahl der Runden 3.

(schon verwendete Buchstaben sind mit Großbuchstaben hervorgehoben, die Buchstaben S und D bezeichnen den Zug der jeweiligen Spieler)

                S       D
 aababba   aabaaBba   aaBaaBba   aaBaaBba
               /       /  /       /  /
ababbaba  ababBaba   aBabBaba   aBaBBaba
              D       S            S

Diese Spiel hat Spoiler in der dritten Runde gewonnen, da D nicht mehr ziehen kann (eine Linie zu dem dritten b im oberen Wort würde eine bestehende Linie kreuzen).

Satz: (Ehrenfeucht und Fraïssé)

Das Spiel Gk(u,v) wird von D gewonnen, wenn u und v durch FOL-Formeln (First-Order-Logic, Prädikatenlogik) der Quantorentiefe k nicht zu unterscheiden sind, d.h. u\models\varphi\Leftrightarrow v\models\varphi für alle φ der Quantorentiefe k.

(Satz entsprechend Vorlesung Automatentheorie)

Meine Werkzeuge