Theorembeweiserpraktikum: Anwendungen in der Sprachtechnologie

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 Isabelle/HOL. 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.

Maximale Teilnehmerzahl: 20

Eine Anmeldung ist nicht erforderlich, aber zu Planungszwecken erwünscht (als kurze E-Mail an Sebastian Ullrich).

Voraussetzungen

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

Für die Übungen an den Rechnern im R -143 brauchen Sie einen gültigen Studentenaccount der ATIS. Bitte prüfen Sie nach, ob Ihr Account funktioniert.

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.

Unterlagen und Programme

Isabelle 2017 ist hier herunterladbar.
Ein gutes Tutorial zu Isabelle/HOL findet sich hier, die meisten Themen werden in der ersten Hälfte des Praktikums behandelt.
Der kurze Stil-Guide für Isabelle darf konsultiert werden; etwa nach dem dritten Termin macht das meiste dort beschriebene Sinn (und was keinen Sinn macht haben wir euch absichtlich nicht erzählt).

Abgabe der Übungsaufgaben

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

Übungen

Wenn nicht anders vermerkt, finden die Übungen jeweils von 14:00 Uhr bis 15:30 Uhr statt.

Datum	Raum	Thema	Unterlagen
17.4.	-143	Einleitung, Deduktion	Folien Aufgabenblatt Isabelle-Rahmen Lösung
24.4.	-143	Quantoren, Fallunterscheidung, Definition, Gleichungen	Folien Aufgabenblatt Isabelle-Rahmen Lösung
8.5.	-143	apply-Skripte, automatische Taktiken, Datentypen, Rekursion und Induktion	Folien Aufgabenblatt Isabelle-Rahmen Lösung
15.5.	-143	allgemeine und wechselseitige Rekursion	Folien Aufgabenblatt Isabelle-Rahmen Lösung
22.5.	-143	induktive Prädikate	Folien Aufgabenblatt Isabelle-Rahmen Lösung
29.5.	-143	Maps, Split-Regeln	Folien Aufgabenblatt Isabelle-Rahmen Lösung
5.6.	-143	Semantik und Projektvorstellung	Folien Sprach-Projekt: 1 2 3
12.6.	-143	Attribute, Typedef, Locales	Folien Sitzung
19.6.	-143	Lifting, Codegenerierung, Koinduktion	Folien Sitzung
26.6.	-143	Koinduktion, (Dokumentenerzeugung), Eigene Objekt-Logiken	Folien Sitzung Aussagenlogik
3.7.	-143	Exkurs: Lean	Folien Sitzung
10.7.	-143	Informationen zur Projektpräsentation	Folien
17.7. 10 Uhr	010	Projektvorstellung
			Alle Folien in einem Dokument
			dito, ohne Overlays (zum Drucken)

Veranstalter

Ehemalige Mitarbeiter
Dr.-Ing. Sebastian Ullrich
Dipl.-Inform. Denis Lohner