Prüfer: Lutz Schröder Beisitzer: Paul Wild

So vorneweg: Prof. Schröder scheint sich hauptsächlich dafür zu interessieren, ob man die Zusammenhänge verstanden hat. Es gab bei mir keine Nachfragen über exakte Beweise (aber druchaus mal kurze Beweis-/Erklärungsskizzen) oder über das Ausführen von Algorithmen. Wichtig waren ihm v.a. wie ausdrucksstark und wie komplex welche Logik ist und warum. Man sollte diesbezüglich auf jeden Fall die Zusammenhänge wiedergeben können.

Wirklich gut habe ich die Prüfung leider nicht mehr im Kopf, aber der Anfang dürfte ganz gut hinkommen. Ich habe ihn auch ungefähr im Gesprächsverlauf aufgeschrieben. Da ich mich leider nicht so sonderlich gut an den gesamten Gesprächsverlauf erinnere, habe ich versucht, den Rest der Prüfung in etwa zu rekonstruieren, aber es könnten trotzdem noch ein paar Fragen fehlen.

Schröder: Wir haben uns in der Vorlesung mehrere Logiken angesehen. Welche? Und beschreiben sie dabei gleich die jeweilige Komplexität.

Ich:

• Aussagenlogik, FOL, Modallogik und Beschreibungslogik, EL;
• Aussagenlogik: Gültigkeit ist NP-vollständig

Schröder hakt ein: Wie würde man denn zeigen, dass es in NP liegt? Und was ist NP überhaupt?

Ich:

• NP = indeterministische Turing-Maschine rät an der richtigen Stelle immer das richtige Ergebnis;
• Die Turing-Maschine nimmt also eine Formel, rät immer die richtige Belegung und erhält damit die Erfüllbarkeit. - Oh. Das ist Erfüllbarkeit nicht Gültigkeit.

Schröder: Genau. Erfüllbarkeit, nicht Gültigkeit. Dann weiter: Wie war das mit den Komplexitäten der anderen?

Ich: FOL ist unentscheidbar; Gültigkeit ist r.e.: Vollständigkeit von Kalkülen in FOL ⇒ „einfach alle Beweise aufzählen“ und dann die letzte Formel nehmen (British Museum Algorithmus); Gültigkeit aber nicht co-r.e.

Schröder: Wie ist das auf endlichen Modellen?

Ich: Endliche Modelle sind r.e. ⇒ Erfüllbarkeit darüber auch; Während Erfüllbarkeit in FOL co-r.e., aber nicht r.e. ist, ist es jetzt andersherum, weil die Vollständigkeit der Kalküle im endlichen FOL nicht mehr gegeben ist.

Schröder: Okay, dann weiter. Wie steht's mit Modallogik? Können Sie da mal die Syntax aufschreiben?

Ich: Syntax hingeschrieben;

Schröder: Wie schwer ist Modallogik?

Ich: PSPACE-vollständig. Erklärung, warum PSPACE-hart und warum in PSPACE. Dabei sind wir auf Tableaux gekommen.

Schröder: Was wäre z.B. nicht in Modallogik ausdrückbar? Und warum?

Ich: Kapitel Bisimilarität aus dem Skript erklärt.

Schröder: Zu Tableaux: Wie funktionieren die Regeln? Können Sie sie bitte aufschreiben und erklären, wann man welche einsetzt? Wie groß kann der Tableaux-Baum werden und warum?

Ich: Regeln erklärt; Baum kann exponentiell groß werden

Schröder: Okay, dann schauen wir uns mal die Ausdrucksstärke der Logiken an. Wie ist es mit der Ausdrucksstärke in FOL? Wie ausdrucksstark ist FOL?

Ich: Man schaut sich die FO-Definierbarkeit an. Z.B. ist Erreichbarkeit nicht FO-definierbar und nicht in FOL ausdrückbar.

Schröder: Und wie zeigt man das?

Ich: Ehrenfeucht-Fraisse-Spiele; Regeln erklärt; Zusammenhang zur m-Äquivalenz erklärt.

Schröder: Und wie ausdrucksstark sind die anderen Logiken? Ich: Modallogik und Beschreibungslogik sind gleich audrucksstark. Sie sind beide ein Teil von FOL und damit ein bisschen weniger ausdrucksstark.

Schröder: Woran sieht man das?

Ich: Standardübersetzung nach FOL erklärt und aufgeschrieben

Schröder: Ausdrucksstärke in EL? Eine Formel, die in EL nicht ausdrückbar ist? Warum ist die Formel nicht in EL ausdrückbar?

Ich: Simulationsstabilität & Materialisator erklärt