Logik in der Informatik
Prof. Dr. Martin Grohe

Logbuch zur Vorlesung Logik in der Informatik

Di, 12.4.2011: Skript S.1-23. Wiederholung Logik der 1.Stufe
Do, 14.4.2011: Skript S.23-36. Wiederholung Logik der 1.Stufe; Kalküle
Di, 19.4.2011: Skript S.37-43. Sequenzenkalkül; Korrektheit des Kalküls; ableitbare Regeln
Do, 21.4.2011: Skript S.43-54. Beispiele ableitbarer Regeln; Widerspruchsfreiheit; Vollständigkeitssatz; Erfüllbarkeitslemma; Terminterpretationen
Di, 26.4.2011: Skript S.54-59. Reduzierte Terminterpretationen; Negationstreue
Di, 3.5.2011: Skript S.59-62. Satz von Henkin; Erweiterungen widerspruchsfreier Mengen um Beispiele
Do, 5.5.2011: Skript S.62-71. Existenz negationstreuer Erweiterungen; Kompaktheitssatz; Erfüllbarkeitsreduktionen; Elimination freier Variablen; Elimination der Gleichheit
Di, 10.5.2011: Skript S.71-79. Skolem Normalform; Klauseln und KNF; Grundterme und Grundinstanzen; Herbrandstrukturen; Satz von Herbrand
Do, 12.5.2011: Skript S.79-82, 101-103. Folgerungen aus dem Satz von Herbrand; Reduktion von prädikatenlogischer auf aussagenlogische Erfüllbarkeit; Anwendung im automatischen Beweisen; Hoare Tripel; partielle und totale Korrektheit
Di, 17.5.2011: Skript S.103-112. Formaler Rahmen; Syntax und Semantik die WHILE-Sprache; Kalkül für partielle Korrektheit; Korrektheitssatz (ohne Beweis); Beweistableaux; Beispiele
Di, 24.5.2011: Skript S.112-123. Beispiel mit while-Schleife und Schleifeninvariante; Kalkül für totale Korrektheit; Korrektheit des Kalküls; Beispiele; Syntax und Semantik der Modallogik
Do, 26.5.2011: Skript S.123-130. Normalformen für die Modallogik; Einbettung der Modallogik in die Logik der 1.Stufe; Kompaktheitssatz; Bisimilarität; Spielcharakterisierung der Bisimilarität
Di, 31.5.2011: Skript S.131-136. Baumabwicklungen von Kripkestrukturen; Bisimulationsinvarianz der Modallogik; Satz von Hennessey-Milner; Endliche Modelleigenschaft und Entscheidbarkeit
Di, 7.6.11: Skript S.136-158. Beweis der Endlichen Modelleigenschaft; Hilbertkalkül für die Modallogik K; Vollständigkeitssatz; Korrespondenztheorie; Multimodallogik; temporale Logik; Dynamische Logik; prädikatenlogische Modallogik
Do, 9.6.11: Skript S.159-164. Nichtaxiomatierbarkeitsresultate für die Logik der 1. Stufe mit Hilfe des Kompaktheitssatzes; die Sätze von Löwenheim-Skolem und der Satz von Löwenheim-Skolem-Tarski; Elementare Äquivalenz und die Theorie einer Struktur
Di, 14.6.11: Skript S.165-172. Isomorphie und elementare Äquivalenz; Nichtstandardmodelle der Arithmetik; Partielle Isomorphismen; quantorenfreie Äquivalenz
Do, 16.6.11: Skript S.172-177. Hin- und Her-Systeme; endliche Isomorphie, Ehrenfeucht-Fraïssé-Spiele; Spielcharakterisierung der endlichen Isomorphie; Satz von Fraïssé
Di., 21.6.11: Skript S.177-180. Satz von Fraïssé, Definierbarkeit der n-Isomorphie.
Do., 23.6.11: Skript S.180-184 Definierbarkeit der n-Isomorphie, Anwendungen des Satzes von Fraïssé, Nichtaxiomatisierbarkeitssätze mit HH-Systemen.
Di., 28.6.11: Skript S. 184-189. Axiomatisierbarkeit im Endlichen, e-Axiomatisierbarkeit, nicht-e-Axiomatisierbarkeit des Graphzusammenhangs.

Last modified: Thu Jun 16 17:30:46 CEST 2011
Martin Grohe