HOME | ENGLISH | IMPRESSUM | KIT

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

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-Studenten: Diese Veranstaltung ist Teil der Module
    • [IN4INSPT] Sprachtechnologien
    • [IN4INFM] Formale Methoden
    • [IN4INPRAK2] Informatik-Praktikum 2
    Für die Veranstaltung erhält man 3 ECTS Punkte.
  • Diplom-Studenten: Diese Veranstaltung ist Teil der Vertiefungsfächer
    • VF 1: Theoretische Grundlagen
    • VF 6: Softwaretechnik und Übersetzerbau
    Die Veranstaltung ist prüfbar in diesen Vertiefungsfächern mit 2 SWS.

Unterlagen und Programme

  • Isabelle/HOL ist hier herunterladbar, die Windows-Version ist auch hier zu finden.
  • Eine gutes Tutorial zu Isabelle/HOL findet sich hier, die meisten Themen werden in der ersten Hälfte des Praktikums behandelt.

Abgabe der Übungsaufgaben

Die Lösungen der Übungen sind über den Praktomaten einzureichen. Der Zugang erfolgt mit den Rechenzentrums-Zugangsdaten.

Übungen

Datum Raum Thema Unterlagen
16.4. -143 Einleitung, Deduktion Folien Aufgabenblatt Isabelle-Rahmen
23.4. -143 Quantoren, Fallunterscheidung, Definition, Gleichungen Folien Aufgabenblatt Isabelle-Rahmen
30.4. -143 apply-Skripte, automatische Taktiken, Datentypen, Rekursion und Induktion Folien Aufgabenblatt Isabelle-Rahmen
7.5. -143 allgemeine und wechselseitige Rekursion Folien Aufgabenblatt Isabelle-Rahmen
14.5. -143 induktive Prädikate Folien Sitzung Aufgabenblatt Isabelle-Rahmen
21.5. -143 Semantik Folien Sitzung Aufgabenblatt Isabelle-Rahmen
28.5. -143 Projektvorstellung Folien Semantics.thy Eulerian.thy
4.6. -143 Attribute, Typedef, Locales Folien Sitzung
18.6. -143 Dokumentenerzeugung, Codegenerierung, Lifting Folien Sitzung
9.7. -143 Informationen zur Projektpräsentation Folien
16.7. 16 Uhr  010 Projektvorstellung
Alle Folien in einem Dokument
dito, ohne Overlays (zum Drucken)

Veranstalter

Lehrstuhlinhaber
Prof. Gregor Snelting
Wissenschaftliche Mitarbeiter
Denis Lohner
Ehemalige Mitarbeiter
Dr. rer. nat. Joachim Breitner