Prinzipiell ist die Stimmung sehr entspannt und der Prüfungstermin kann bei geringer Teilnehmerzahl (meistens der Fall) sehr flexibel abgesprochen werden. Zu Beginn der Prüfung wird erklärt, wie eine mündliche Prüfung abläuft (siehe Prüfungsprotokolle von LBS). Hier sei nochmal betont, dass Fragen stellen während der Prüfung, wenn man eine Frage nicht verstanden hat, kein Problem ist.

Was man ansonsten wissen sollte: MMT ist in dieser Prüfung SEHR wichtig. Wenn man da noch Schwierigkeiten/Lücken hat, dann empfiehlt es sich, das PDF-Tutorial oder das Tutorial auf der Webseite durchzumachen.

Q: „Erklären Sie Aussagenlogik und schreiben Sie diese in MMT auf.“

A: Ich habe die Idee hinter Prädikatenlogik erklärt, dabei Natural Deduction kurz angerissen, bevor ich angefangen habe, sie in MMT zu implementieren. Nach 2-3 Operatoren hat Prof. Kohlhase gemeint, dass es reicht, da er sieht, dass ich das Prinzip verstanden habe.

Q: „Ok, das reicht soweit. Formalisieren Sie dann doch bitte auch Natural Deduction in MMT.“

A: Daraufhin habe ich ein paar der Regeln formalisiert, aber auch hier waren nicht sehr viele gefragt.

Q: „Das reicht erstmal. Angenommen, Sie haben folgende Konstante <schreibt eine MMT-Konstante auf> und möchten folgendes Regel <schreibt MMT-Zeile auf> zeigen. Wie machen Sie das?“ (Ich weiß das Beispiel nicht mehr genau, aber von der Idee her dürfte es ähnlich zu folgendem gewesen sein: const: {a, b} ⊦ a ∧ b jDD zu zeigen: a ∨ b)

A: In unserem Beispiel dürfte es auf etwas ähnliches wie „proof: {a, b} ⊦ (a ∨ b) = orIntro AndElim const “ hinauslaufen.

Q: „Okay, gehen wir weiter zu FOL. Wie funktioniert FOL und wie formalisiert man sie in MMT?“

A: Kurz erklärt, wie man Prädikatenlogik zu FOL umbaut und auch den zusätzlichen Typ und forall formalisiert.

Q: „Und wie könnte man 'exists' definieren?“

A: Ich habe exists wie in der Übung formalisiert, wichtig war dabei auch die tatsächliche Definition.

Q: „So, dann möchten wir jetzt einmal eine tatsächliche mathematische Theorie definieren, z.B. Monoid. Diesmal am Besten mitsamt Kopfzeile.“

(Ich war mir der Mathematik hinter Monoid noch ein wenig unsicher und habe daher nachgefragt. Prof. Kohlhase meinte aber, dass das kein Problem sei, da es nicht darum gehe, die mathematischen Strukturen auswendig zu können, sondern um das Formalisieren und hat sie mir genannt.) A: Dann habe nachgefragt, ob/welche Theorie wir dafür includen wollen und anschließend Monoid formalisiert wie in den Folien, aber ohne Subtheorien.

Q: „Dann gehen wir doch mal über zur Mengentheorie. Wie funktioniert die?“

A: Ich habe dann die Brücke geschlagen von FOL über HOL zu ZF. Als ich dabei war, ZF zu erklären, meinte er, dass es reicht, wenn ich 3 Axiome aus ZF nennen und erklären würde. Und 2 davon solle ich formal aufschreiben. (nicht MMT, sondern in Higher Order Logik wie im Skript)

Q: „Zusatzfrage am Ende: Was hat ⊢ in mmt für einen Typ?“

A: predicate → type

Nachtrag: Irgendwo während des Prüfungsgesprächs kamen noch Fragen zum Curry-Howard-Isomorphismus bzw. wie/wo er in MMT angewandt wird. (Das dürfte relativ wichtig gewesen sein!)