Mo, 31.10.11: Folien 65-80. Beweis des Stazes über
die funktionale Vollständigkeit; Adäquatheit und neue Junktoren;
Negationsnormalform; konjunktive und disjunktive Normalform;
Kompaktheitssatz (ohne Beweis)
Mi, 2.11.11: Folien 80-83. Beweis des
Kompaktheitssatzes; Anwendung auf Färbarkeit unendlicher
Graphen; Umwandlung in erfüllbarkeitsäquivalente KNF in
Linearzeit
Mo, 7.11.10: Folien 84-99. Resolventen;
Resolutionslemma; Resolutionswiderlegungen; Korrektheit und
Vollständigkeit der Resolution; Komplexität des
aussagenlogischen Erfüllbarkeitsproblems;
Erfüllbarkeitsalgorithmen, insbesondere DPLL
Mi, 9.11.10: Folien 100-108. Beispiel für einen Lauf des
DPLL-Algorithmus; Hornformeln; Streichungsalgorithmus; Einführung in die
Logikprogrammierung und Prolog;
Mo, 14.11.11: Folien 109-120. Fakten; Anfragen; Regeln;
Beispielprogramme; Terme; Substitutionen; Grundterme;
Ableitungen; deklarative Semantik; Rekursion: Beispiele rekursiver
Programme und rekursiver Datentypen; Zusammenhang von Graphen;
natürliche Zahlen in Unärkodierung;
Mi, 16.11.11: Folien 120 -129. Listen; Binäre
Suchbäume; Aussagenlogik in Prolog implementiert; operationale
vs deklarative Semantik; einfacher Interpreter für Logikprogramme;
Beweis der Korrektheit des einfachen Interpreters (Induktionsanfang für (1) --> (2))
Mo, 21.11.11: Folien 129-132. Beweis der Korrektheit des
einfachen Interpreters (Fortsetzung); Unifikation; allgemeinste
Unifikatoren;
Mi, 23.11.11: Folien 133-137. Unifikationsalgorithmus; Beispiele zum
Unifikationsalgorithmus; Interpreter für Logikprogramme mit
Unifikation; Interpreter für reines Prolog;
Mi, 30.11.11: Folien 155-165. Beispiele von Strukturen;
Strukturen aus
Logikprogrammen; Restriktionen und Expansionen; Isomorphie;
Mo, 5.12.11: Folien 166-181.
Syntax der Logik der 1. Stufe; Freie
Variablen; Belegungen und Interpretationen; Semantik der Logik
der 1. Stufe; Koinzidenzlemma
Mi, 7.12.11: Folien 182-201. Beispiele;
Isomorphielemma; die von einer Formel
definierte Relation; Erfüllbarkeit; Allgemeingültigkeit;
Folgerungsbeziehung; Äquivalenz; Substitutionen; Substitutionslemma (ohne Beweis);
Mo, 12.12.11: Folien 200, 202-208. Beweis des Substitutionslemmas für Terme;
Beweis des Substitutionslemmas für Formeln; Umbenennen
gebundener Variablen; Negationsnormalform;
Mi, 14.12.11: Folien 209-213. Äquivalenzen; Pränexe Normalform
Wiederholung
Logik der 1. Stufe; Ableitungen und Kalküle
Mo, 2.1.12: Folien 214-224. Abgeschlossene
Mengen in Kalkülen; Sequenzenkalkül für die Logik der ersten
Stufe; Korrektheit
Mi, 25.1.12: Folien
244-251. Grundterme und Grundatome; Herbrandstrukturen; Satz
von Herbrand; Reduktion des prädikatenlogischen auf das
aussagenlogische Erfüllbarkeitsproblem
Mo, 30.1.12: Folien
252-260. Beweis des Reduktionssatzes; automatische
Theorembeweiser; Prädikatenlogische Resolution; Logikprogrammierung und die
Logik der 1.Stufe;
Mi, 1.2.12: Folien 261-271. Nullestellige Relationen.
Übersetzung von Logikprogrammen in die Logik der
ersten Stufe; Modelltheoretische Charakterisierung der
Semantik von Logikprogrammen;
Mo, 6.2.12: Folien 272-276.
minimale Herbrandmodelle; modelltheoretische
Sichtweise auf Anfragen; Semi-Entscheidbarkeit des
Allgemeingültigkeits und des Folgerungdproblems;
Mi, 8.2.12: Folien 277-283.
Unentscheidbarkeit der Logik der 1.Stufe; Simulation von Turingmaschinen durch Logikprogramme
Mo, 13.2.12: Kurze Wiederholung der gesamten Vorlesung.
