Dozent: Ralf Möller
Ort: TUHH, Harburger Schloßstraße 20, Raum 206
Zeit: Dienstag 10.45-13.00 Uhr
Uebung (Alissa Kaplunova)
Inhalt:
- Einführung und Motivation, Aussagenlogik, Syntax, Semantik, Wahrheitstabellen, Entscheidungsprobleme
- Boolesche Algebra, Resolution für Aussagenlogik, Anwendungen
- Prädikatenlogik erster Stufe, Syntax, Semantik, Entscheidungsprobleme (Teil 1)
- Prädikatenlogik erster Stufe, Entscheidungsprobleme (Teil 2), Anwendung: Konzeptuelle Datenmodellierung
- Anwendung: Algorithmenverifikation
- Unifikation, Resolution für Prädikatenlogik
- Anwendung: Wumpus-Welt, First-Order-Modellierung von Aktionen
- Temporale Logiken I (lineare Zeit)
- Temporale Logiken II (verzweigende Zeit)
- TLA: Temporal Logic of Actions
- Beschreibungslogik I
Einführung, Syntax, Semantik, Entscheidungsprobleme, - Beschreibungslogik II
Tableau-basierte Entscheidungsverfahren - Berechenbarkeit (Kurzeinführung)
Unentscheidbare Probleme am Beispiel des Halteproblems für Turing-Maschinen - Beschreibungslogik III
Komplexität der Entscheidungsprobleme - Temporale Beschreibungslogik (nicht in WS 05)
- Beschreibungslogik und Aktionen (nicht in WS 05)
Danksagungen:
Präsentationen für Aussagenlogik und Pädikatenlogik nach dem Buch von wurden von Uwe Schöning (s.u.) wurden von Javier Esparza übernommen. Einige Präsentation stammen auch von Uwe Schmidt. Die Folien der Wumpus-Anwendung sowie für die Resolution sind von Jörg Desel nach dem Buch "Artificial Intelligence, a Modern Approach" (St. Russel und P. Norwig) erstellt worden.
Die Folien zur Temporalen Logik sind einer Vorlesung von Wolfram Kahl entnommen. Präsentationen zu TLA sind aus Vorträgen von John Akinyemi, Massimiliano Menarini und Christopher Schulte kombiniert worden.
Von Franz Baader habe ich die Präsentationen zur Beschreibungslogik übernommen.
Vielen Dank für die Bereitstellung.
Literatur:
- Uwe Schöning, Logik für Informatiker,
Spektrum Akad. Vlg., Hdg. Erscheinungsdatum: 2000, Auflage: 5. Aufl., ISBN: 3827410053 - M. Huth, M. Ryan, Logic in Computer Science, Modeling and Reasoning about Systems,
Cambridge University Press, 2000 - Leslie Lamport, Specifying Systems, The TLA+ Language and Tools for Hardware and Software Engineers
- F. Baader et al. (Hrsg.), Description Logic Handbook, Cambridge
University Press, 2003
NB: Um Mißverständnissen vorzubeugen: Für die Klausur ist der Inhalt dieser Vorlesung maßgebend. Es reicht nicht,
zur Vorbereitung einfach nur eine Literaturangabe aus der Obigen Liste zu wählen.
Ralf Möller