In diesem Praktikum soll der Einsatz eines Theorembeweisers erlernt werden und schließlich selbstständig zur Formalisierung und Verifikation eines Projekts aus dem Bereich der Sprachtechnologie verwendet werden. Der verwendete Theorembeweiser ist der Beweisassistent Lean 4, der an unserem Lehrstuhl mitentwickelt wird. In der ersten Hälfte des Praktikums erlernt man anhand von Übungsblättern die wichtigsten Prinzipien im Theorembeweisen, z.B. Deduktion, Simplifikation, Rekursion, induktive Definitionen. In der zweiten Hälfte des Praktikums soll in Teams selbstständig ein Thema im Bereich der Sprachtechnologie, z.B. Semantik, Typsysteme, Compiler, formalisiert und verifiziert werden.

Die Übungsblätter werden einzeln, das vollständige Projekt als Gruppenarbeit bearbeitet und abgegeben. Die Anwesenheit an allen Übungsterminen, bei der Projektvorstellung und -präsentation wird erwartet. Es gibt keine begleitende Vorlesung für dieses Praktikum. Es muss keine schriftliche Praktikums- oder Projektausarbeitung erstellt werden.

Das Praktikum wird dieses Semester vollständig online auf der Platform gather.town durchgeführt. Weitere Informationen dazu werden wir den angemeldeten Teilnehmern per E-Mail zukommen lassen. Der erste Praktikumstermin ist der 13.4.2021 um 14:00.

Maximale Teilnehmerzahl: 20

Zur Anmeldung bitten wir um eine kurze E-Mail an Jakob von Raumer.

Voraussetzungen

Kenntnisse in Logik, funktionaler Programmierung und formalen Systemen sind vorteilhaft, aber nicht zwingend.

Einordnung

Master Informatik SPO 2015: Das Praktikum kann als Modul Theorembeweiserpraktikum: Anwendungen in der Sprachtechnologie [M-INFO-102666] in den Vertiefungsfächern Theoretische Grundlagen und Softwaretechnik und Übersetzerbau sowie im Wahlbereich mit 3 ECTS-Punkten angerechnet werden.

Abgabe der Übungsaufgaben

Die Lösungen der Übungen sind über den Praktomaten einzureichen. Der Zugang erfolgt mit Ihrem KIT-Account.

Unterlagen

Datum	Unterlagen
13.4.	Organisatorisches
1.6.	Projektvorstellung
6.7.	Informationen zur Projektpräsentation

Alle weiteren Materialen finden sich in unserem Praktikums-Repository.

Als Forum mit weiteren Informationen und mehr Austausch dient uns Zulip (siehe Info-Mail).

Veranstalter

Ehemalige Tutoren
Marc Huisinga

Wissenschaftliche Mitarbeiter
Dr. Jakob von Raumer

Ehemalige Mitarbeiter
Dr.-Ing. Sebastian Ullrich