Logik

Evaluation:

Kurs im Wintersemester 2009/10 von  Till Mossakowski 

K 4 SWS 
Mo von 12:00 - 14:00 MZH 1400
Do von 14:00 - 16:00 MZH 5210
Präsentation der Lösungen von Übungsaufgaben: in der Vorlesung oder in einem freiwilligen Zusatztermin mittwochs von 8-10h (Beginn: 04.11.) in Sportturm C 5130. die Termine am 20.1., 27.1. und 3.2. fallen aus!!!
Beginn der Vorlesung: 19.10.2009
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).
Buch und CD sind z.B. in der Uni-Buchhandlung erhältlich.

Scheinkriterien

Hinweis zum Grade grinder: die der CD beiliegende Nr. muss unter "Registration ID" eingegeben werden. Unter "Instructor's Name" muss "Till Mossakowski", und unter "Instructor's Email Address" muss "till@informatik.uni-bremen.de" eingegeben werden. "Your name" und "Your Email address" sind selbsterklärend - aber Achtung: diese dürfen sich für eine bestimmte Registration-ID nicht mehr ändern, sondern müssen stets gleich bleiben.

Mindmap vom 22.10.2009

Übungen

• Übungen Kapitel 1 bis 2.4: Abgabe bis 03.11.2009, je nach Typ der Aufgabe per Grade grinder oder per Mail oder in Postfach 99.
• Übungen Kapitel 2.5 bis Kapitel 6: Abgabe bis 10.11.2009
• Übungen Kapitel 7 bis Kapitel 8: Abgabe bis 17.11.2009, 12h
• Zusätzliches Übungsblatt mit weiteren Aufgaben für Note 1 (Abgabe: 17.11.09, 12h)
• Übungen Kapitel 9 bis Kapitel 10.2: Abgabe bis 24.11.2009, 12h
• Übungen Kapitel 10.3 bis Kapitel 12 sowie Zusatzaufgabe Spezifikation von Tarski's world in CASL: Abgabe bis 1.12.2009, 12h
• Übungen Kapitel 13 + 16.27 - 16.31 sowie Zusatzaufgabe: schreibe ein Java-Programm annotiert mit JML, so dass All- und Existenzquantoren verwendet werden. Abgabe bis 8.12.2009, 12h
• Übungen Kapitel 18. Abgabe bis 15.12.2009, 12h
• Übungen Kapitel 17.4-17.16, 19.1-19.23. Abgabe verlängert bis 12.01.2010, 12h
• restliche Übungen: Kapitel 14, 15, 16.1-16.26, 17.17-17.45, 19.24-19.34. Abgabe 26.01.2010, 12h, Vorrechnen 28.01.2010