FB 3 | ||||||
AG BKB > Lehre > WS 11/12 > | ||||||
Logik |
||||||
Kurs im Wintersemester 2011/12 von Till Mossakowski und Lutz Schröder K
4 SWS 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 Übungen (Abgabe per Grade grinder oder über logic.informatik...)
Folien
CASL und Hets
|
||||||
Autor: Dr. Till Mossakowski |
||||||
AG BKB |
|