TU München - Fakultät für Informatik

Vorlesung | Sommersemester 2007
Perlen der Informatik 2
Prof. Tobias Nipkow

News

• Einen Interpreter für den λ-Kalkül gibt es hier.
• Ab dem 24.5. wird die Übung rechnergestützt stattfinden. Wer einen Laptop hat möge diesen bitte mitbringen, und vorher Isabelle installieren (s.u.)

Inhalt

In der Vorlesung werden ausgewählte Themen aus verschiedenen Bereichen der (hauptsächlich theoretischen) Informatik angesprochen:

• Primzahltests
• Unifikation
• Lambda-Kalkül
• Logik
• Interaktives Beweisen
• Funktionale Programmierung
• Endliche Automaten
• Entscheidungsverfahren für Arithmetik

Hörerkreis: Teilnehmer am Begabtenförderungsprogamm der Fakultät und andere Interessierte.

Voraussetzungen: keine

Literatur

• Michael Huth and Mark Ryan. Logic in Computer Science. Cambridge University Press.

Übungsblätter

• 1. Übungsblatt (PDF)
• 2. Übungsblatt (PDF)
• 3. Übungsblatt: [ PDF | Isabelle-Theorie ]
• 4. Übungsblatt (PDF)
• 5. Übungsblatt: [ PDF | .thy | .thy (ohne x-symbols) ]
• 6. Übungsblatt: [ PDF | .thy | .thy (ohne x-symbols) ]
• 7. Übungsblatt: [ PDF | .thy | .thy (ohne x-symbols) ]
• 8. Work in progress: RedBlackTree.thy, RedBlackTree_Insert.thy, RedBlackTree_Delete.thy

Isabelle

Für einige Übungen werden wir den interaktiven Beweiser Isabelle einsetzen. Isabelle ist auf der Rechnerhalle (rayhalle) installiert und kann dort wie folgt gestartet werden:

Wer Isabelle auf dem eigenen Rechner installieren will, findet die nötigen Pakete samt Installationsanleitung unter http://isabelle.in.tum.de/dist-Isabelle_07-May-2007. Man braucht dafür Linux und einen installierten XEmacs.

Als Alternative gibt es unter obiger URL auch eine fertige Installation in einer virtuellen Maschine (ein komplettes Linux mit Isabelle und allen benötigten Komponenten), die sich dann auch unter Windows verwenden lässt.

Falls Schwierigkeiten bei der Installation auftreten, meldet euch bei mir (krauss(at)in.tum.de).

Unterlagen zu Isabelle