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:
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
Christoph Lüth
Last modified: Fri Apr 5 18:16:36 CEST 2002