Di, 27.10.09:
Skript S.31-39. Widerspruchsfreiheit; Vollständigkeitssatz; Erfüllbarkeitslemma;Terminterpretationen und reduzierte Terminterpretationen
Do, 29.10.09:
Skript S.39-43. Satz von Henkin; Formelmengen, die Beispiele
enthalten
Di, 3.11.09:
Skript S.43-48.
Negationstreue Erweiterungen; Kompaktheitssatz;
Erfüllbarkeitsäquivalenz; Erfüllbarkeitsreduktion von beliebigen Formeln auf Sätze;Erfüllbarkeitsreduktion
auf gleicheitsfreie Formeln
Do, 5.11.09: Skript S.49-54. Skolem Normalform;
Klauseln und KNF; Grundterme und Grundinstanzen; Herbrandstrukturen
Di, 10.11.09: Skript S.54-59. Satz von Herbrand und seine Konsequenzen; Reduktion von prädikatenlogischer
auf aussagenlogische Erfüllbarkeit;
Anwendung im automatischen Beweisen; Substitutionen
Do, 12.11.09: Skript S.60-66. Algebraische
Eigenschaften von Substitutionen; Unifikation
Di, 17.11.09: Skript S.66-71.Effizienz der
Unifikation; Unifikation von Mengen von Termen oder Literalen;
prädikatenlogische Resolution; Korrektheit; Lifting Lemma
Do, 19.11.09: 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
Di, 24.11.09: Skript S.78-82.
Korrektheit des partiellen Korrektheitskalküls;Beweistableaux; Beispiele
Di, 1.12.09: Skript S.82-91.
Kalkül für totale Korrektheit; Korrektheit des
Kalküls; Beispiele; Syntax und Semantik der Modallogik
Do, 3.12.09: Skript S.91-97.
Einbettung der Modallogik in die Logik der 1.Stufe; Kompaktheitssatz;
Bisimilarität; Spielcharakterisierung der Bisimilarität
Di, 8.12.09:
Skript S.95-104. Baumabwicklungen von Kripkestrukturen;
Bisimulationsinvarianz der Modallogik; Satz von
Hennessey-Milner; Endliche Modelleigenschaft und Entscheidbarkeit
Do, 10.12.09:
Skript S.102-109.
Hilbertkalkül für die Modallogik K; Vollständingkeitssatz; Logic Engineering
Di, 15.12.09: Skript S.110-114.
Korrespondenztheorie; Syntaktischer und Semantischer Zugang zu speziellen
Modallogiken; Wissens- und Glaubenslogik; Korrepondenzsatz; Gödel-Löb-Logik
Di, 5.1.10: Skript S.121-125. 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; Beschreibung endlicher
Strukturen in der Logik der ersten Stufe
Do, 7.1.10:
Skript S.125-131. Isomorphie und elementare Äquivalenz;
Nichtstandardmodelle der Arithmetik; Partielle Isomorphismen; quantorenfreie Äquivalenz;
Hin- und
Her-Systeme
Di, 12.1.10:
Skript S.131-137. Beispiel für Hin- und Her-System, endliche Isomorphie, Ehrenfeucht-Fraïsé-Spiele, Spielcharakterisierung der endlichen Isomorphie, Satz von Fraïssé
Do, 14.1.10: Skript S.137-140. Definierbarkeitslemma;
Beweis des Satzes von Fraïssé; Folgerungen aus dem Definierbarkeitslemma
Di, 19.1.10: Skript S.140-142. Nichtaxiomatierbarkeitsergebnisse mit
dem Satz von Fraïssé
Do, 21.1.10: Skript S.143-148. Axiomatiersbarkeit und
Nichtaxiomatisierbarkeit im
Endlichen; Abstände und Umgebungen
in Strukturen; lokale Formeln und basislokale Sätze; Satz von
Gaifman (ohne Beweis)
Di, 26.1.10: 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, 28.1.10: 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, 2.2.10: Skript
S.168-171. Σ1-Transfersatz; Repräsentierbarkeit in arithmetischen Theorien
Do, 4.2.10: Skript
S.172-177.
Repräsentierbarkeit der berechenbaren Funktionen und
entscheidbaren Relationen in Q; Fixpunktsatz; Unmöglichkeit der Selbstrepräsentierbarkeit
einer Theorie; Nichtdefinierbarkeit der Wahrheit
Di, 9.2.10: Skript
S.178-184.
Unentscheidbarkeit der Logik der 1.Stufe; Erster Unvollständigkeitssatz; die Beweisbarkeitsformel einer
Theorie; Gödelsätze; das Hilbertsche Programm; Konsistenzsatz einer Theorie; Peano Arithmetik; Eigenschaften
der Beweisbarkeitsformel; Satz von Löb (ohne Beweis); Zweiter Unvollstädnigkeitssatz
Do, 11.2.10: Skript
S.183-185. Beweis des Satzes von Löb; Verbindung zur Modallogik und der
Vollständigkeitssatz von Solovay; kurze Wiederholung der ganzen Vorlesung
Last modified: Thu Feb 18 14:07:52 CET 2010
Martin Grohe
