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

Ehemalige Mitarbeiter
Dipl.-Inform. Denis Lohner