Prüfer / Beisitzer:

• Lutz Schröder
• Daniel Hausmann

Note 2.3

Prüfungsatmosphäre wahr ok. Schröder erwartete recht genaue Antworten half aber aus wenn es hing. Die Benotung war sehr fair. Der Inhalt der Prüfung war leider schon im vorhinein festgelegt. Schröder hatte ein Blatt mit ca. 10-15 Fragen dabei und hat die so ziemlich abgearbeitet. Viele interessantere Themengebiete aus FOL (E-F, m-Äquivalenz, Gültigkeit und Erfüllbarkeit von FOL), ALC (PSPACE Beweis mittels Reduktion von TQBF) und EL (Materialisator) kamen leider garnicht zur Sprache. Das war echt schade, da das mein Lernfokus war. Stattdessen haben wir dann viel Zeit mit Aussagenlogik verbracht, was ich in der Vorlesung eigentlich nur als Recap (aus Glolop) empfunden habe. Da die Note zu 50% davor schon feststeht ob der Übungsnote kann man auch nicht mehr soviel holen. Der Sinn davon erschliesst sich mir garnicht. Hoffentlich hilft jemanden das Protokoll. - GreenBourne

• Syntax von Aussagenlogik angeben
  • Habe versehentlich NNF angegeben. Sollte diese dann bennen und danach die Syntax der allgemeinen Aussagenlogik angeben.
• Ist Erfüllbarkeit in Aussagenlogik in Polynomzeit entscheidbar? (SAT-Problem)
  • Nein denn der Algorithmus liegt nicht in P sondern in NP.
• Warum ist es in NP?
  • Nicht deterministische Turing Maschine kann in polynomieller Zeit Problem lösen.
    • Wie lautet der Algorithmus?
      • Bei jedem Atom die 'richtige' Belegung wählen.
• Mit welchem Mittel der Wahl hat man stattdessen Erfüllbarkeit in Aussagenlogik gezeigt?
  • Tableaux. Regeln anmalen und Semantik erklären (u.a. groß Gamma).

• Syntax von Modallogik

• Modell der Wahl?
  • Kripkemodelle.

• Wie sieht zusätzliche Tableaux Regel aus? Anzeichnen.
  • Warum gilt diese?
    • Einfach anhand von Kripkerahmen erklären, dass Regel gilt.
• Wie groß kann Tableaux in Abhängigkeit von Formelgröße werden?
  • Exponentiell groß. (Siehe Übung)
• Was ist eine Simulation?
  • Diagramm dazu anzeichnen.
• Was ist eine Bisimulation?
  • Simulation in beide Richtungen mit selber Menge an Tupeln nur vertauscht (siehe Skript).
• Was bedeuted bisimulationsinvariant?
  • Bisimilare Zustände erfüllen die selben Modalformeln.
• Warum ist ALC Teil von FOL?
  • Es gibt eine Übersetzungsfunktion von FOL nach ALC.
    • Übersetzungsfunktion hinzeichnen.
• Warum ist FOL Aussagekräftiger als ALC?
  • Das einelementige reflexive Kripkemodell ist bisimilar zum Modell der unendlich verkettete Liste. Diese Modelle sind daher nicht unterscheidbar in ALC. In FOL dagegen aber schon.