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 verwandt 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.

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.
  Es gibt folgende zwei GUIs für Isabelle: ProofGeneral und I3P
• ProofGeneral wird mit Isabelle mitgeliefert, Aufruf im Poolraum "/usr/local/Isabelle/bin/isabelle emacs". Für die Formelsyntax auf den Poolrechnern im Menü ProofGeneral -> Options -> Unicode-Tokens aktivieren; auf anderen Systemen muss man manchmal stattdessen XSymbols aktivieren.
• I3P ist hier herunterladbar. Isabelle wird mittels Isabelle -> Start Prover gestartet. Beim ersten Mal muss man den Pfad zu Isabelle angeben. Für den Poolraum geht das folgendermaßen: Manage Configurations -> Add -> Unix Installation of Isabelle auswählen, dann Next -> Pfad /usr/local/Isabelle/ angeben, dann Next -> Isabelle 2009 auswählen, dann Next -> HOL auswählen, dann Finish. Bei anderen Installationen ist das analog, es muss nur der passende Isabelle-Pfad angegeben werden.
• Eine gutes Tutorial zu Isabelle/HOL findet sich hier, die meisten Themen werden in der ersten Hälfte des Praktikums behandelt.

Termine

vom 13.04.2010, bis 13.07.2010

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

Übungen

Datum	Thema	Unterlagen
13.4.	Einleitung + Deduktion	Folien, Aufgabenblatt, Isabelle-Rahmen
20.4.	Quantoren + Simplifikation	Folien, Aufgabenblatt, Isabelle-Rahmen
27.4.	Rekursion	Folien, Aufgabenblatt, Isabelle-Rahmen
4.5.	allgemeine Rekursion	Folien, Aufgabenblatt, Isabelle-Rahmen
11.5.	Induktive Prädikate	Folien, Aufgabenblatt, Isabelle-Rahmen
18.5.	Isar	Folien, Aufgabenblatt, Isabelle-Rahmen
25.5.	Isar/Fortsetzung	Folien, Aufgabenblatt, Isabelle-Rahmen
1.6.	Projektvorstellung	Folien, Semantik-Theorie

Veranstalter

Ehemalige Mitarbeiter
Dr.-Ing. Daniel Wasserrab