HOME | ENGLISH | IMPRESSUM | KIT

Theorembeweiserpraktikum: Anwendungen in der Sprachtechnologie

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 -abschlussbesprechung 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

  • 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 2SWS.
  • Master-Studenten: Diese Veranstaltung ist Teil der Module
    • [IN4INSPT] Sprachtechnologien
    • [IN4INFM] Formale Methoden
    Für die Veranstaltung erhält man 3 ECTS Punkte.

Unterlagen und Programme

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

Termine

vom 12.04.2011, bis 12.07.2011

Tag Beginn Ende Ort
Dienstag 14:00h 15:30h Praktikumspool -143, Geb. 50.34

Übungen


Datum Thema Unterlagen
12.4. Einleitung + Deduktion Folien, Aufgabenblatt, Isabelle-Rahmen
19.4. Quantoren + Simplifikation Folien, Aufgabenblatt, Isabelle-Rahmen
26.4. Rekursion Folien, Aufgabenblatt, Isabelle-Rahmen
3.5. allgemeine Rekursion Folien, Aufgabenblatt, Isabelle-Rahmen
10.5. induktive Prädikate Folien, Aufgabenblatt, Isabelle-Rahmen
17.5. Isar Folien, Aufgabenblatt, Isabelle-Rahmen
24.5 Isar/Fortsetzung Folien, Aufgabenblatt, Isabelle-Rahmen
31.5. Projektvorstellung Folien, Semantik-Theorie

Veranstalter

Wissenschaftliche Mitarbeiter
Denis Lohner