Prüfer: Lutz Schröder, Daniel Hausmann

• Welche Logiken haben wir betrachtet?
• Wie ist die Komplexität von FOL?
  • Unentscheidbar; Gültigkeit r.e.; Erfüllbarkeit co-r.e
• Warum ist Gültigkeit r.e.?
  • Beweise aufzählen?
• Welche Eigenschaft ist dafür notwendig?
  • Vollständigkeit von Beweiskalkül
• Was passiert mit Erfüllbarkeit bei endlichen Modellen?
  • r.e.
• Cool, dann ist FOL auf endlichen Modellen entscheidbar, oder?
  • Nein, Gültigkeit nicht mehr r.e.
• Gibt's eine Formel, die nur in unendlichen Modellen erfüllbar ist?
  • Ja, man muss so ein paar Eigenschaften fordern, wie irreflexibilität, transitivität, usw
• Und eine, die nur in endlichen?
  • ¬ von der vorherigen
• Was haben wir gemacht um die Ausdrucksstärke zu analysieren?
  • FO-Derfinierbarkeit
• Wie zeigt man sowas?
  • Ehrenfeucht-Fraïssé-Spiele. Erklären.
  • E-F-S ⇒ ≃m
  • Dann kam Nachfrage nach Umkehrung
  • Antwort: Mit endlichem Σ
• Welche Klassen haben wir beispielsweise so angeschaut?
  • ORD und EVEN

• Bisimulation?
  • Bisimilare Zustände erfüllen die selben Modalformeln.
• Welche Umkehrungen gibt es und gelten die?
  • Zustände, die die gleichen Modalformeln erfüllen, sind bisimilar.
  • Nur in endlich verzweigten Modellen (Hennessy/Milner)
• Beispiel für unendiche Modelle, wo es nicht gilt?
  • Das Beispiel aus dem Skript
• Algo für Erfüllbarkeit?
  • Tableaux. Erklären, ¬□-Regel hinzeichnen
• Welche Platzschranke und warum?
  • PSPACE. Stacktiefe * Stackframe
• Geht's besser?
  • Nein, PSPACE-hart
• Wie zeigt man das?
  • Reduktion
• Welche Reduktionen haben wir für PSPACE-härte gemacht?
  • TQBF (Quantorenbaum) → Modalformel
• Wie ging das ungefähr?
  • Formel bauen, so dass Quantorenbaum Modell und man aus Modellen für die Formel Quantorenbäume extrahieren kann.

• Welche Komplexität?
  • PTIME
• Algo?
  • Materialisator. erklären, wie und warum.
• Simulationsstabilität?
  • erklären
• Modalformel, die nicht in EL?
  • □⊥