Prüfer: Lutz Schröder, Daniel Hausmann

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.

• Syntax von Aussagenlogik angeben
  • Habe versehentlich NNF angegeben. Sollte diese dann bennen und danach die wirkliche Syntax 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.

• Weitere Tableaux Regel anzeichnen
  • Warum gilt die? Einfach anhand von Kripkerahmen erklären.
• Wie gross kann Tableaux in Abhängigkeit von Formel werden?
  • Exponentiell gross.
• 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 die gleichen Formeln würden nicht mehr gelten. Damit wäre Modallogik aber nicht mehr bisimulationsinvariant. Not sure. Bitte fixen^^