TU Wien:Higher-order Logic VU (Leitsch)

Daten

Vortragende	Alexander Leitsch• Martin Riener
ECTS	3,0
Letzte Abhaltung	2024W
Sprache	English
Mattermost	higher-order-logic • Register • Mattermost-Infos
Links	tiss:192040

Zuordnungen

Masterstudium Logic and Computation

Modul Logic, Mathematics, and Theoretical Computer Science (Gebundenes Wahlfach)

Inhalt

• (Kurze) Wiederholung First-order Logic + Sequent Calculus LK
• Syntax und Semantik von Second-order Logic + Calculus $LK_{2}$
• Diverse Eigenschaften und Theoreme von 2nd Order-Logic (z.B. Löwenheim-Skolen und Compactness gilt nicht mehr)
• Verschiedene Systeme der Arithmetik
  • Model-theoretic approach
    • True Arithmetik ($TA{\text{ bzw. }}A$)
    • 2nd-order Arithmetik ($A_{2}$)
  • Proof-theoretic approach
    • Minimale Arithmetik $Q$
    • 1st-order Peano Arithmetik ($PA_{1}$)
    • 2nd-order Peano Arithmetik ($PA_{2}$)
• Typisierter Lambda Kalkül
• Higher-order Logic + Calculus $LK_{\omega }$
• Überblick über Automated Deduction in HOL (kam nicht zur Prüfung)

Ablauf

Prof Leitsch trägt im Monolog den Stoff aus seinen Folien vor und rechnet hin und wieder Beispiele an der Tafel vor. Zusätzlich zum Foliensatz gibt es allerdings ein ausführliches Skriptum, in welchem jedes einzelne Tafelbeispiel sauber und vollständig dokumentiert ist. Dementsprechend braucht man bei den Beispielen nicht mitzuschreiben, sondern kann sich aufs Verständnis konzentrieren, was auch von Herrn Leitsch so empfohlen wurde.

Benötigte/Empfehlenswerte Vorkenntnisse

Es wird de facto erwartet, den Kurs Logic and Computability VU bereits abgeschlossen zu haben. Zwar wird vieles noch einmal neu erklärt, jedoch ist man ohne Vorkenntnisse zu First-order Logic, Sequent Calculus (Calculus LK) und diversen Theoremen aus dem erwähnten Fach schnell etwas überfordert. (Anmerkung: geschrieben aus der Sicht von jemandem, der L&C parallel zu Higher-order logic gemacht hat)

Prof. Leitsch ist aber wirklich sehr bemüht, auf Fragen von Studenten einzugehen und alles möglichst verständlich zu erklären.

Vortrag

Prof. Leitsch geht meistens in einem angenehmen Tempo durch den Stoff (manchmal etwas zügig, gerade bei neuen Notationen, wo es sich oft lohnt, ihn mit Fragen etwas auszubremsen). Er bemüht sich aber generell sehr, das Verständnis der Studenten zu fördern. Tafelbeispiele müssen wie erwähnt nicht mitgeschrieben werden (stehen fast 1:1 so im Skript).

Übungen

Eine Handvoll Übungsblätter, die für üblich einen überschaulichen Umfang haben.

Außerdem sind die Übungsblätter freiwillig. In den Übungsstunden (die alle paar Wochen statt der Vorlesung stattfinden), rechnen freiwillige Studenten die Beispiele vor. Meldet sich niemand, rechnet Prof. Leitsch das Beispiel selbst vor. Ihm ist wichtig, dass die Übungsstunden wirklich keine Prüfungssituation sind, sondern eine Möglichkeit, um aus Fehlern zu lernen.

Generell eine sehr angenehme Atmosphäre in den Übungsstunden.

Prüfung, Benotung

Die komplette Note hängt von der mündlichen Prüfung am Ende ab. Termin nach Vereinbarung.

Prof. Leitsch nennt dies aber nur ungern Prüfung sondern eher "Fachgespräch" und beginnt mit einfachen Fragen, auf denen er dann kontinuierlich mit schwierigeren Fragen aufbaut. Sein Ziel sei, dass man auch während der Prüfung noch Neues dazulernen kann, so seine eigene Aussage.

Die mündliche Prüfung war sehr fair. Prof. Leitsch zielte komplett auf Verständnisfragen zum Stoff ab und wollte keine Details zu mathematischen Beweisen wissen (nur eine sehr grobe Idee der Herleitung und schlussendlich bewiesene Aussage). Ich durfte während der Prüfung an einem Whiteboard stehen und diverse Formel zur Untermalung meiner Antworten aufschreiben. Manchmal sind seine Fragen fast etwas zu allgemein und abstrakt, was wiederum verwirren kann, daher sollte man wirklich ein gutes Verständnis für die second- und higher-order logic aufgebaut haben. Benotung war aber wirklich sehr fair.

Dauer der Zeugnisausstellung

Die Note wir einem direkt nach der Prüfung mündlich mitgeteilt. Zeugnisausstellung vermutlich erst, wenn alle Studenten ihre mündliche Prüfung abgeschlossen haben (wie erwähnt: Termin für jeden einzeln nach Vereinbarung).

Zeitaufwand

Vergleichsweise ziemlich gering, da die wenigen Übungsaufgaben komplett freiwillig sind und der Stoff meiner Meinung nach auch recht überschaubar war. Ich habe zwei Tage auf die Prüfung gelernt und ein Sehr Gut bekommen.

Unterlagen

noch offen

Tipps

Skriptum gut mitlesen über das Semester hinweg und frühzeitig fragen stellen (war auch per E-Mail immer sehr gut möglich).

Keine Beweise auswendig lernen, sondern sich auf das generelle Verständnis konzentrieren.

Highlights / Lob

Super fand ich, dass alle Tafelbeispiele ohne Abstriche im Skriptum dokumentiert sind. Daher musste man nie mitschreiben (außer kleine Notizen), was beim Verständnis erheblich geholfen hat.

Verbesserungsvorschläge / Kritik

Vorlesungsunterlagen wurden jede Woche per E-Mail geschickt, was oft etwas klobig ist. Es wäre schön, wenn man den Kurs auf denselben Stand wie nahezu alle anderen Kurse bringen könnte -> Kurs im TUWEL anlegen. Wenn dort auch Abgaben für die Übungen eingerichtet werden, bringt auch das mehr Übersichtlichkeit für die Studierenden, die für üblich halt doch einige Kurse gleichzeitig machen.

Außerdem war im WS2024 der letzte Teil zu Automated Deduction (der aber wie angekündigt nicht zur Prüfung kam) leider recht unvorbereitet und das hat man auch gemerkt. Wird aber wahrscheinlich nächstes Jahr viel besser sein.

Materialien

Diese Seite hat noch keine Anhänge, du kannst aber neue hinzufügen.