Do, 25.10.07:
Skript S.26-34.Korrektheit des Sequenzenkalküls; ableitbare
Regeln; Eigenschaften widerspruchsfreiere und
widerspruchsvoller Formelmengen
Di, 30.10.07:
Skript S.34-42.Vollständigkeitssatz; Erfüllbarkeitslemma;
Terminterpretationen und reduzierte Terminterpretationen; Satz
von Henkin; Erweiterungen um Beispiele
Do, 1.11.07:
Skript S.42-48.Negationstreue Erweiterungen von Formelmengen;
Beweis des Erfüllbarkeitslemmas; Kompaktheitssatz; Erfüllbarkeitsreduktionen;
Erfüllbarkeitsreduktion von beliebigen Formeln aus Sätze
Di, 6.11.07:
Skript S.47-53.Erfüllbarkeitsreduktion auf gleicheitsfreie
Formlen; Skolem Normalform; Klauseln und KNF
Do, 8.11.07:
Skript S.53-58. Satz von Herbrand und seine Konsequenzen;
Anwendung im automatischen Beweisen
Di, 13.11.07:
Skript S.56-65. Reduktion von prädikatenlogischer
auf aussagenlogische Erfüllbarkeit; algebraische
Eiogenschaften der Substitution; Unifikation und allgemeinste Unifikatoren; Unifikationsalgorithmus
Do, 15.11.07:
Skript S.66-71. Effizienz der Unifikation; Unifikation von
Mengen von Termen oder Literalen; Prädikatenlogische
Resolution; Korrektheit; das Lifting Lemma
Di, 20.11.07:
Skript S.71-78. Vollständigkeit der Resolution; resolutionsbasierte
Theorembeweiser; Hoare Tripel; partielle und totale Korrektheit; formaler
Rahmen; Syntax und Semantik die WHILE-Sprache; Kalkül für partielle Korrektheit
Do, 22.11.07:
Skript S.78-82. Korrektheit des partiellen Korrektheitskalküls;
Beweistableaux; Beispiele
Di, 27.11.07:
Skript S.82-91. Kalkül für totale Korrektheit; Korrektheit des
Kalküls; Beispiele; Syntax und Semantik der Modallogik
Do, 29.11.07:
Skript S.91-96.Einfache Eigenschaften der Modallogik;
Einbettung in die Logik der 1.Stufe; Kompaktheitssatz;
Bisimilarität; Spielcharakterisierung der Bisimilarität
Di, 4.12.07:
Skript S.96-103. Baumabwicklungen von Kripkestrukturen;
Bisimulationsinvarianz der Modallogik; Satz von
Hennessey-Milner; Endliche Modelleigenschaft und Entscheidbarkeit
Do, 6.12.07:
Skript S.101-108. Beweis der endlichen Modelleigenschaften;
Hilbertkalkül für die Modallogik K; Vollständingkeitssatz
Do, 13.12.07:
Skript S.113-122. Die Beweislogik GL; Multimodallogik; temporale Logik;
Dynamische Logik; prädikatenlogische Modallogik;
Nichtaxiomatierbarkeitsresultate für die Logik der 1. Stufe mit
Hilfe des Kompaktheitssatzes
Di, 18.12.07:
Skript S.123-128. Die Sätze von Löwenheim-Skolem und der Satz von
Löwenheim-Skolem-Tarski; Elementare Äquivalenz; Nichtstandardmodelle der Arithmetik
Do, 20.12.07:
Skript S.128-130. Partielle Isomorphismen; quantorenfreie Äquivalenz;
die Existenz des Weihnachtsmannes
Di, 8.1.08: Skript S.131-135. Hin- und
Her-Systeme; n-Äquivalenz und endliche Äquivalenz;
Ehrenfeucht- Fraïssé-Spiele; Satz von Fraïssé
Do, 10.1.08:
Skript S.136-139. Beweis des Satzes von Fraïssé, insbesonder Definierbarkeit der n-Isomorphie
Di, 15.1.08: Skript S.139-145. Folgerungen aus dem
Definierbarkeitslemma; Nichtaxiomatierbarkeitsergebnisse mit
dem Satz von Fraïssé; Axiomatiersbarkeit im Endlichen
Do, 17.1.08:
Skript S.144-152. Nichtaxiomatisierbarkeit im Endlichen der Klasse der
endlichen zusammenhängenden Graphen; Abstände und Umgebungen
in Strukturen; lokale Formeln und basislokale Sätze; Satz von Gaifman
Di, 22.1.08: Skript S.152-159. Beweis des Satzes
von Gaifman zu Ende geführt; Kodierung von Formeln und anderen
syntaktischen Objekten ("Gödelisierung"); Theorien und
Enscheidbarkiet; effektive
Axiomatisierbarkeit; spezielle Kodierung für die Sprache der Arithmetik
Do, 24.1.08: Skript S.159-164. Aufzählbarkeit und
Entscheidbarkeit definierbarer Zahlenmengen; beschränkte
Formeln; Lemma über die β-Funktion; berechenbare Funktionen
Di, 29.1.08: Skript
S.164-168. Σ1-Definierbarkeit berechenbarer
partieller Funktionen und rekursiv aufzählbarer Relationen;
die Minimale Arithmetik Q; Korrektheit von Q; der Σ1-Transfersatz
Do, 31.1.08: Skript
S.168-172. Beweis des Σ1-Transfersatzes (zu
Ende); Repräsentierbarkeit in arithmetischen Theorien;
Repräsentierbarkeit der berechenbaren Funktionen und
entscheidbaren Relationen in Q
Di, 5.2.08: Skript
S.172-177. Beweis des Repräsentierbarkeitssatzes;
Fixpunktsatz; Unmöglichkeit der Selbstrepräsentierbarkeit
einer Theorie; Nichtdefinierbarkeit der Wahrheit
Do, 7.2.08: Skript
S.177-184. Unentscheidbarkeit der Logik der 1.Stufe; der
erste Unvollständigkeitssatz; die Beweisbarkeitsformel einer
Theorie; Gödelsätze; das Hilbertsche Programm; 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
Last modified: Mon Feb 11 10:20:34 CET 2008
Martin Grohe
