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 (was bedeutet gross Gamma etc).

• Syntax von Modallogik

• Modell der Wahl? Kripkemodelle.

• Wie sieht zusätzliche Tableaux Regel aus? Anzeichnen.
  • Warum gilt die? Einfach anhand von Kripkerahmen erklären, dass Regel gilt.
• Wie gross kann Tableaux in Abhängigkeit von Formelgröße werden?
  • Exponentiell gross.
• Was ist eine Simulation? Diagramm dazu anzeichnen.
• Was ist eine Bisimulation?
  • 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 aber es wären nicht die gleichen Formeln erfüllt in diesen Modellen. Damit wäre Modallogik aber nicht mehr bisimulationsinvariant. Bin mir nicht sicher, ob diese Begründung stimmt.