==== OntoSWeb WS14/15 ==== Prüfer: Lutz Schröder, Daniel Hausmann == FOL == * 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 == ALC == * 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. == EL == * Welche Komplexität? * PTIME * Algo? * Materialisator. erklären, wie und warum. * Simulationsstabilität? * erklären * Modalformel, die nicht in EL? * □⊥