Gedächtnisprotokoll zur Diplomprüfung Theoretische Informatik

• Wie sind die aussagenlogischen Formeln definiert?
• Was ist eine Belegung?
• Wie ist die Auswertungsfunktion definiert?
• Ich hatte die Klammern bei den aussagenlogischen Formeln vergessen. Daher kam die Nachfrage: Was liefert <>(a b c)?
  • Der Ausdruck ist nicht definiert, da wir keine Prioritätenregelung besitzen. Man muß klammern.
• Wann heißt eine Formel erfüllbar?
• Wie kann man die Erfüllbarkeit einer Formel prüfen?
  • Mit der Wahrheitstafelmethode.
• Wie lange dauert dies?
  • Die Methode benötigt mindestens (n-1)*2^n elementare Operationen.
• Kann man es schneller berechnen?
  • Das weiß man nicht, denn das Erfüllbarkeitsproblem ist NP-vollständig.
• Nennen Sie eine Version des Kompaktheitssatzes der Aussagenlogik.
  • Ich nannte die positive Variante, woraufhin ich auch noch nach der negativen gefragt wurde.
• Prof. Weihrauch erläuterte die Definition der prädikatenlogischen Terme, Atome und Formeln und fragte, was wir für die Semantik der Prädikatenlogik brauchen.
  • Struktur, Termauswertungsfunktion und Wahrheitswertefunktion.
    Alle drei mußte ich erläutern, bei den Funktionen war aber die Abbildungsvorschrift das Wichtigste. Die Definition der Funktionen habe ich nur angedeutet.
• Was bedeuten die Ausdrücke S a(), S a, a?
  • Hierbei sollte ich die Bedeutung mit Hilfe der Funktion WW ausdrücken.
• Was bedeutet "t frei für y in a"?
• Was ist ein Herbrand-Universum, eine Herbrand-Struktur?
• Wie lautet der Satz von Löwenheim-Skolem?
• Können Sie dies beweisen?
• Sind die allgemeingültigen PF entscheidbar, beweisbar, ...?
  • Wir entwickelten gemeinsam einen Beweis zur Beweisbarkeit der allgemeingültigen Formeln, wobei ich die Bildung der Pränexnormalform verbal erläutern und eine Skolemisierung an einem kleinen Beispiel zeigen mußte.
• Zum Begriff der Theorie wurde ich folgendes gefragt: Definition, Beispiele, Berechnungsmethoden (über Struktur oder Formelmenge).
• Prof. Weihrauch machte einige Bemerkungen zu Nicht-Standard-Modellen.
• Legt eine Theorie die zugehörige Struktur eindeutig fest?
  • Nein, wie aus dem Beweis von Löwenheim-Skolem für unendliche Strukturen ersichtlich ist.