Prüfer / Beisitzer:

• Lutz Schröder
• Daniel Hausmann

Note 2.3

Prüfungsatmosphäre wahr ok. Schröder erwartete recht genaue Antworten half aber 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 wie E-F, m-Äquivalenz, Gültigkeit und Erfüllbarkeit in FOL, EL, Materialisator, PSPACE von bestimmtem Modallogiken kamen leider garnicht dran. Sowie deren Beweise. Das war echt schade. Stattdessen haben wir dann viel Zeit mit Aussagenlogik verbracht, was ich in der Vorlesung eigentlich nur als Recap empfunden habe. Da die Note zu 50% davor schon feststand durch die Übungen kann man auch nicht mehr soviel holen. Der Sinn davon erschliesst sich mir garnicht aber gut. Hfftl hilft jemanden das Protokoll.

PS: Wenn jemand Fehler findet in den Antworten, bitte ergänzen :)

• Syntax von Aussagenlogik angeben
  • Habe versehentlich NNF angegeben. Sollte diese dann bennen und danach die Syntax der allgemeinen Aussagenlogik angeben.
• Ist Aussagenlogik erfüllbar? (SAT)
  • Nein. NP vollständig.
• Warum ist es in NP?
  • Nicht deterministische Turing Maschine kann in polynomieller Zeit Problem lösen.
    • Algo? 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ß.
• 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?
  • In ALC kann man xRx nicht darstellen.
  • Begründung: Ich glaube es wären alle Modelle bisimilar zum einelementigen reflexiven Kripkemodell. Da diese Modelle aber nicht die gleichen Modalformeln erfüllen wäre Modallogik nicht mehr bisimulationsinvariant (Widerspruch nach Lemma). Bin mir nicht sicher, ob diese Begründung exakt so stimmt.