Gödel, Escher, Bach, Isabelle.

LOGIK: Gödel, Escher, Bach, Isabelle.

Willkommen auf der Heimatseite der Logikveranstaltung. Diese Seite dient als Startpunkt zu den im Netz verfügbaren Informationen zu dieser Lehrveranstaltung.

Inhalt der Lehrveranstaltung

Diese Lehrveranstaltung spannt den Bogen von der Theorie (Prädikatenlogik erster und zweiter Stufe) bis hin zu den praktischen Anwendungen und Auswirkungen der Logik sowohl in der Informatik als auch z.B. in der Kunst. Während Gödels Unvollständigkeitssatz die Grenzen dessen aufzeigt, was auf einer Maschine berechenbar ist, erlauben Theorembeweiser wie Isabelle die voll formale und damit maschinell prüfbare Spezifikation, Verifikation und Entwicklung von Software.

Die Lehrveranstaltung beginnt mit einer Wiederholung der Prädikatenlogik erster Stufe und einer Einführung der Prädikatenlogik zweiter Stufe. Danach kann der Kurs praktisch orientiert mit einem Praktikum für den Theorembeweiser Isabelle, oder theoretisch und dennoch anschaulich dargestellt mit einer Einführung der Gödelisierung, Selbstbezüglichkeit und mancher Antinomien bis hin zu der Bedeutung des Unvollständigkeitssatzes von Gödel, fortgesetzt werden.

Organisatorisches

Die Lehrveranstaltung hat einen Umfang von vier Wochenstunden. In der ersten Hälfte des Semesters findet die Veranstaltung zweimal wöchentlich statt. In der zweiten Hälfte kann dann zwischen dem theoretischen Teil mit dem gleichen Format, und dem Isabelle-Praktikum mit einer wöchentlichen Veranstaltung und zusätzlichen Rechnerübungen gewählt werden.

Termine:

Mo, 13-15 MZH 6240 Isabelle-Praktikum

Mo, 13-15 MZH 5300 Theoret. Kurs

Do, 13-15 MZH 5290 Theoret. Kurs

Informationen zum Theoretischen Teil

Skript

Hier findet man das Skript der Veranstaltung.

Literaturverzeichnis Logik

H. J. Kreowski: Logische Grundlagen der Informatik.
Verlag R. Oldenbourg, München 1991.
Uwe Schöning: Logik für Informatiker.
Spektrum Akademischer Verlag GmbH, Berlin Oxford 1995.
B. Heinemann, K. Weihrauch: Logik für Informatik.Eine Einführung.
B.G.Teubner Verlag, Stuttgart 1992.
Douglas R. Hofstadter: Gödel, Escher, Bach. Ein Endloses Geflochtenes Band
Ernst Klett Verlag, Stuttgart, 1979.

Informationen zu Isabelle

Folien und Übungsblätter

Die Folien zu den Vorträgen (werden ständig aktualisiert). Hier sind die Übungsblätter:

[1] in der revidierten Fassung vom 22.06.98, und das Beweisskript fuer die dritte Aufgabe. Dazu die Musterlösung.
[2], ausgegeben am 29.06.98, und die Theorie Animals.thy.
[3], ausgegeben am 06.07.98.
[4], ausgegeben am 13.07.98, und die Theorie Primes.thy mit Primes.ML.

Technisches

Isabelle wird gestartet mit dem folgenden Befehl:

/usr/local/pub-bkb/isabelle/Isabelle98/bin/isabelle

Die Theorie gcd.thy, die in der ersten Stunde als Beispiel vorgestellt wurde, nebst den zugehörigen Folien.

Literatur und Links zu Isabelle

A Gentle Introduction to Isabelle Eine kurzes und verständliches tutorial für die ersten Schritte mit Isabelle. Leider etwas veraltet.
Introduction to Isabelle. Eine ausführlichere und weitergehende Einführung.
Das Kapitel über HOL aus dem Handbuch der Isabelle-Objektlogiken.
Isabelle's Referenz-Handbuch.
On-line Dokumentation der Isabelle-Logiken, hier und in München.
Die Isabelle-Heimseiten in Cambridge und München.

Christoph Lüth

Last modified: Fri Apr 5 18:16:36 CEST 2002

Mo, 13-15	MZH 6240	Isabelle-Praktikum
Mo, 13-15	MZH 5300	Theoret. Kurs
Do, 13-15	MZH 5290	Theoret. Kurs