Logik

K 4 SWS 
Mo von 13:00 - 15:00 GW2 B1410 (nicht mehr parallel in MZH 5210) ,
Do von 13:00 - 15:00 GW2 B1410
Beginn: 25.10.2007
VAK: 03-05-H-604.02
ECTS: 6

Logik wird in der Informatik an vielen Stellen eingesetzt, und zwar immer da, wo etwas formal in seinen Eigenschaften beschrieben werden soll (z.B. Programme, Sprachen, Graphen, Netzwerkprotokolle, Agenten, ...). Basierend auf solchen logischen Beschreibungen ist es dann auch möglich, Beweise zu führen (neben den Beweisen, die ihr aus der Mathematik kennt, auch z.B. Programm- oder Protokollverifikation). Außerdem kann man sogar in Logik direkt programmieren (vgl. Prolog), und das sehr problemnah.

Diese Vorleseung führt in die Prädikatenlogik erster Stufe ein, die in vieler Hinsicht grundlegend ist. Themen sind: Aussagen- und Prädikatenlogik, logische Formalisierung, logische Folgerung, Spiele zum Herausfinden von Wahrheitswerten, was ist ein Beweis?, Beweiskalküle, Korrektheit, Vollständigkeit, Anwendungen in der Informatik (Programmverifikation, Prolog).

Als Grundlage soll das Buch "Sprache, Beweis und Logik'' von Jon Barwise und John Etchemendy (CSLI Stanford) dienen. Es ist didaktisch sehr gut aufgebaut und vor allem ist zusätzlich eine CD mit vier Programmen erhältlich, die es möglich machen, selbst am Computer Übungen zur Logik durchzuführen. Zudem gibt es über einen Server in Stanford direktes Feedback zu den Lösungen. Das Buch und die Software wurden national und international schon sehr erfolgreich an vielen anderen Unis eingesetzt. Es ist inzwischen im Mentis-Verlag auch in deutscher Übersetzung erschienen. Buch und auch die CD werden ein zentraler Bestandteil dieser Vorlesung sein.

Lokale Informationen zum Buch und zur Software (nur innerhalb des FB3 zugreifbar, oder durch Einloggen auf einem FB3-Rechner und Benutzung von lynx).

Scheinkriterien

Folien

• 25.10.2007
• 29.10.2007
• 01.11.2007
• 08.11.2007
• 15.11.2007
• 22.11.2007
• 29.11.2007
• 06.12.2007
• 13.12.2007
• 20.12.2007
• 10.01.2008 JML
• 17.01.2008
• 24.01.2008
• 31.01.2008
• 07.02.2008

Übungen

• Übungen zu Kapitel 1 und 2: Abgabe am 05.11.2007 bis 13h, je nach Typ der Aufgabe per Grade grinder oder per Mail. Welche noch auf die Bestellung der CD warten, können ausnahmsweise auch die Grinder-Übungen an mich mailen.
• Übungen zu Kapitel 3 und 4: Besprechung am 12.11. und 19.11.2007, Abgabe bis 19.11.07, 10h, per Grade grinder oder (bei den Aufgaben mit freiformuliertem Text) per mail.
• Übungen zu Kapitel 5 bis 8: Besprechung am 19.11. und 26.11.2007, Abgabe bis 26.11.07, 10h. Für 6.40-6.42 darf Taut Con benutzt werden.
• Übungen 17.17 bis 17.45 sowie Logelei und Sudoku: Besprechung am 26.11. und 03.12.2007, Abgabe bis 03.12.07, 10h
• CASL-Datei Blocks.casl
• Heterogeneous Tool Set. Bei Benutzung des Java-Installers bitte den daily shnapshot von hier herunterladen, mit bunzip2 entpacken, ausführbarmachen und das alte hets in lib/hets damit ersetzen.
• Übungen Kapitel 9 und Kapitel 10, 10.1 bis 10.19: Besprechung am 03.12. und 10.12.2007, Abgabe bis 10.12.07, 10h
• Übungen Kapitel 10, 10.20 bis 10.31, Kapitel 11 und 12: Besprechung am 10.12. und 17.12.2007, Abgabe bis 17.12.07, 10h
• Übungen Kapitel 13: Besprechung am 17.12.2007 und 07.01.2008, Abgabe bis 07.01.08, 10h
• Übungen Kapitel 16 bis 16.26: Besprechung am 07.01.2008 und 14.01.2008, Abgabe bis 14.01.08, 10h
• Übungen Kapitel 16, 16.27 bis 16.31, JML-Spezifikation, Listen-Induktion: Besprechung am 14.01.2008 und 21.01.2008, Abgabe bis 21.01.08, 10h
• Übungen Kapitel 18, 18.1 bis 18.19,Besprechung am 21.01.2008 und 28.01.2008, Abgabe bis 28.01.08, 10h
• Übungen Kapitel 18, 18.20 bis 18.30, Besprechung am 28.01.2008 und 04.02.2008, Abgabe bis 04.02.08, 10h
• Übungen 17.4 - 17.16 und Kapitel 19, Besprechung am 04.02.2008, Abgabe bis 11.02.08