Di, 21.10.08:
Skript S.27-34. Ableitbare
Regeln; Eigenschaften widerspruchsfreier und
widerspruchsvoller Formelmengen; Vollständigkeitssatz; Beweis
des Vollständigkeitssatzes aus dem Erfüllbarkeitslemma
Do, 23.10.08:
Skript S.34-40. Beweis des Erfüllbarkeitslemma;
Terminterpretationen und reduzierte Terminterpretationen;
Negationstreue
Di, 28.11.08:
Skript S.41-46.Negationstreue Erweiterungen von Formelmengen und
Erweiterungen, die Beispiele enthalten; Satz von Henkin;
Beweis des Erfüllbarkeitslemmas; Kompaktheitssatz;
Erfüllbarkeitsreduktionen;
Erfüllbarkeitsreduktion von beliebigen Formeln aus Sätze
Do, 30.10.08: Skript S.46-54.Erfüllbarkeitsreduktion
auf gleicheitsfreie Formlen; Skolem Normalform; Klauseln und KNF;
Grundterme und Grundinstanzen
Di, 4.11.08:
Skript S.54-60. Satz von Herbrand und seine Konsequenzen; Reduktion von prädikatenlogischer
auf aussagenlogische Erfüllbarkeit;
Anwendung im automatischen Beweisen; die algebraische Struktur
von Substitutionen
Do, 6.11.08: Skript S.61-68. Unifikation
Di, 11.11.08:
Skript S.66-71. Effizienz der Unifikation; Unifikation von
Mengen von Termen oder Literalen; Prädikatenlogische
Resolution; Korrektheit; das Lifting Lemma; Vollständigkeit der Resolution; resolutionsbasierte
Theorembeweiser
Do, 13.11.08:
Skript S.73-80. Hoare Tripel; partielle und totale Korrektheit; formaler
Rahmen; Syntax und Semantik die WHILE-Sprache; Kalkül für partielle
Korrektheit; Korrektheit des partiellen Korrektheitskalküls
Di, 18.11.08:
Skript S.80-85. Beweistableaux; Beispiele; Kalkül für totale Korrektheit; Korrektheit des
Kalküls; Beispiele
Do, 20.11.08:
Skript S.87-95. Syntax und Semantik der Modallogik; einfache Eigenschaften der Modallogik;
Einbettung in die Logik der 1.Stufe; Kompaktheitssatz;
Bisimilarität
Di, 25.11.08:
Skript S.95-101. Spielcharakterisierung der Bisimilarität; Baumabwicklungen von Kripkestrukturen;
Bisimulationsinvarianz der Modallogik; Satz von
Hennessey-Milner; Endliche Modelleigenschaft und Entscheidbarkeit
Do, 27.11.08:
Skript S.102-108. Beweis der endlichen Modelleigenschaft;
Hilbertkalkül für die Modallogik K; Vollständingkeitssatz
Do, 4.12.08:
Skript S.114-122. Multimodallogik; temporale Logik;
Dynamische Logik; prädikatenlogische Modallogik;
Nichtaxiomatierbarkeitsresultate für die Logik der 1. Stufe mit
Hilfe des Kompaktheitssatzes
Di, 9.12.08:
Skript S.122-128. Nichtaxiomatisierbarkeit des Zusammenhangs
von Graphen; die Sätze von Löwenheim-Skolem und der Satz von
Löwenheim-Skolem-Tarski; Elementare Äquivalenz; Nichtstandardmodelle der Arithmetik
Do, 11.12.08:
Skript S.128-134. Partielle Isomorphismen; quantorenfreie Äquivalenz;
Hin- und
Her-Systeme; n-Isomorphie und endliche Isomorphie;
Ehrenfeucht- Fraïssé-Spiele
Di, 16.12.08:
Skript S.134-140. Beweis der Spielcharakterisierung von
endlicher Isomorphie; Satz von Fraïssé;
Definierbarkeitslemma
Do, 18.12.08: Skript S.140-145. Nichtaxiomatierbarkeitsergebnisse mit
dem Satz von Fraïssé; Axiomatiersbarkeit und
Nichtaxiomatisierbarkeit im
Endlichen
Di, 6.1.09:
Skript S.146-149. Abstände und Umgebungen
in Strukturen; lokale Formeln und basislokale Sätze; Satz von
Gaifman; disjunkte Vereinigungen von Strukturen
Do, 8.1.09: Skript S.149-153. Beweis des Satzes
von Gaifman
Di, 13.1.09: Skript S.155-165.
Kodierung von Formeln und anderen
syntaktischen Objekten ("Gödelisierung"); Theorien und
Enscheidbarkiet; effektive
Axiomatisierbarkeit; spezielle Kodierung für die Sprache der
Arithmetik; Aufzählbarkeit und
Entscheidbarkeit definierbarer Zahlenmengen; beschränkte
Formeln; Lemma über die β-Funktion (ohne Beweis);
berechenbare Funktionen; Δ0-Definierbarkeit
von Berechnungen
Do, 15.1.09: Skript
S.166-167. Σ1-Definierbarkeit berechenbarer
partieller Funktionen und rekursiv aufzählbarer Relationen;
Beweis des Lemmas über die β-Funktion;
die Minimale Arithmetik Q; Korrektheit von Q
Di, 20.1.09: Skript
S.168-171. Σ1-Transfersatz; Repräsentierbarkeit in arithmetischen Theorien
Do, 22.1.09: Skript
S.172-175.
Repräsentierbarkeit der berechenbaren Funktionen und
entscheidbaren Relationen in Q
Di, 27.2.09: Skript
S.176-181. Fixpunktsatz; Unmöglichkeit der Selbstrepräsentierbarkeit
einer Theorie; Nichtdefinierbarkeit der Wahrheit;
Unentscheidbarkeit der Logik der 1.Stufe; der
erste Unvollständigkeitssatz; die Beweisbarkeitsformel einer
Theorie; Gödelsätze; das Hilbertsche Programm
Do, 29.1.09: Skript
S.181-189. der
Konsistenzsatz einer Theorie; Peano Arithmetik; Eigenschaften
der Beweisbarkeitsformel; Satz von Löb; der zweite
Unvollständigkeitssatz; Verbindung zur Modallogik und der
Vollständigkeitssatz von Solovay; Syntax und Semantik der
Logik der 2.Stufe, monadische Logik der 2.Stufe
Di, 3.2.09: Skript
S.189-195. Ausdrucksstärke der Logik der 2.Stufe;
Unentscheidbarkeit; Scheitern von Komapktheit,
Vollstädnigkeit, Löwenheim-Skolem; reguläre Sprachen; Wörter
asl Strukturen und Definierbarkeit von Sprachen; Satz von
Büch, Elgot und Trachtenbrot; eine Beweisrichtung
Do, 5.2.09: Vorlesung wegen Krankheit ausgefallen
Di, 10.2.09: Vorlesung wegen Krankheit ausgefallen
Do, 12.2.09: Kurze Wiederholung der gesamten Vorlesung
Last modified: Thu Feb 12 10:53:34 CET 2009
Martin Grohe
