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