In dieser Vorlesung über Beweisassistenten treffen sich Studierende der Informatik, Mathematik und Computerlinguistik.
Beweisassistenten werden in der Chipherstellung und Softwareentwicklung eingesetzt, um die Fehlerfreiheit von Soft- und Hardware zu verifizieren. Sie geben MathematikerInnen letzte Gewissheit, wenn sie ihren eigenen Beweisen nicht trauen. Für LinguistInnen sind sie eine Möglichkeit mit Typentheorie zu experimentieren - einem Formalismus, der auch zur Modellierung der Semantik natürlicher Sprache verwendet wird.
Die Vorlesung bietet eine bündige Einführung in die Funktionsweise von Beweisassistenten und ihre theoretischen Grundlagen. Dazu zählen zum Beispiel der Lambda-Kalkül, Typentheorie inklusive induktiver Typen und die Curry-Howard-Korrespondenz. Zudem schauen wir uns beispielhaft an, wie Beweisassistenten und Typentheorie für die oben genannten Anwendungen eingesetzt werden können.
In den Übungen wird die Theorie erfahrbar anhand von Lean, einem modernen Beweisassistenten, der in der jüngsten Formalisierungswelle innerhalb der Mathematik eine maßgebende Rolle spielt.
Im Studiengang "Mathematik und Anwendungsgebiete" wird diese Veranstaltung im Rahmen des Moduls "Ausgewählte Kapitel der Algebra/Geometrie" angeboten.
So bekommen Sie die Lean-Übungsblätter: Öffnen Sie den cgbf2023-Ordner in VSCode oder öffnen Sie ihr Codespaces-Projekt. Klicken Sie auf die kreisförmigen Pfeile unten links neben dem Wort "main". Nun finden Sie das neue Übungsblatt im Ordner src/CGBF/Uebungen/. Die Lösungen werden eine Woche später auch in diesem Ordner veröffentlicht.
Um die Leistungspunkte für das Modul zu erhalten, müssen Sie eine schriftliche Klausur (ohne Computer) bestehen. Um an der Klausur teilnehmen zu können, müssen Sie die Zulassung erhalten. Zulassungsvoraussetzung sind 50% der Übungsblätter-Punkte.
Studierende der Computerlinguistik können auch Beteiligungsnachweise erwerben. Dazu müssen sie die Zulassungsvoraussetzung erreichen. Die Klausur muss dafür nicht geschrieben werden.
Die Klausuren werden ähnlich gestaltet sein wie die Probeklausur: Probeklausur (Lösung). Insbesondere werden die Klausuren auch die beiden Spickzettel der Probeklausur enthalten.