Mi, 17.10.12: Folien 1-30. Paradoxien; Syllogismen;
Anwendungen der Logik in der Informatik; Syntax der Aussagenlogik; Semantik(Vorbereitung); Semantik der
Aussagenlogik
Mo, 22.10.12: Folien 31-52. Rekursive Definitionen über Formeln;
Koinzidenzlemma; Wahrheitstafeln; Erfüllbarkeit;
Allgemeingültigkeit; Folgerungsbeziehung; aussagenlogische
Modellierung von Sudoku; Anwendung
Schaltkreisverifikation
Mo, 29.10.12: Folien 62-76. funktionale Vollständigkeit;
Adäquatheit Beweis des Stazes über
die funktionale Vollständigkeit; Adäquatheit und neue Junktoren;
Negationsnormalform; konjunktive und disjunktive Normalform
Mi, 31.10.12: Folien 77-81. Kompaktheitssatz; Beweis des
Kompaktheitssatzes; Anwendung auf Färbbarkeit unendlicher
Graphen
Mo, 5.11.12: Folien 81-91. Beweis des Satzes über die Färbbarkeit von unendlichen Graphen;
Umwandlung in erfüllbarkeitsäquivalente KNF in
Linearzeit; Resolventen;
Resolutionslemma; Resolutionswiderlegungen; Korrektheit und
Vollständigkeit der Resolution
Mi, 7.11.12: Folien 21-104. Komplexität des
aussagenlogischen Erfüllbarkeitsproblems;
Erfüllbarkeitsalgorithmen, insbesondere DP-Algorithmus; Beispiel für einen Durchlauf des
DP-Algorithmus; Hornformeln; Streichungsalgorithmus; Beispiele; Korrektheit des Streichungsalgorithmus (ohne Beweis)
Mo, 12.11.12: Folien 104-119. Beweis des Satzes über die Korrektheit des Streichungsalgorithmus; Einführung in die
Logikprogrammierung und Prolog; Fakten; Anfragen; Regeln;
Beispielprogramme; Terme; Substitutionen; Grundterme
Ableitungen
Mi, 14.11.12: Folien 120 -129. Rekursion: Beispiele rekursiver
Programme und rekursiver Datentypen; Zusammenhang von Graphen;
natürliche Zahlen in Unärkodierung; Deklarative Semantik; 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, 19.11.12: Folien 129-134. Beweis der Korrektheit des
einfachen Interpreters (Fortsetzung); Unifikation; allgemeinste
Unifikatoren; Unifikationsalgorithmus; Beispiele zum
Unifikationsalgorithmus
Mi, 21.11.12: Folien 134-141. Interpreter für Logikprogramme mit
Unifikation; Interpreter für reines Prolog; nichtterminierende
Prologberechnungen
Mo, 26.11.12: Folien 142-155. Suchbäume; Cut; Unifikation in
Prolog; Symbolmengen; Strukturen; Beispiele von Strukturen
Mi, 28.11.12: Folien 155-171. Beispiele von Strukturen;
Strukturen aus
Logikprogrammen; Restriktionen und Expansionen; Isomorphie
Mo, 3.12.12: Probeklausur
Mi, 5.12.12: Folien 172-183.
Syntax der Logik der 1. Stufe; Freie
Variablen; Belegungen und Interpretationen; Semantik der Logik
der 1. Stufe; Koinzidenzlemma
Mo, 10.12.12:
Folien 183-195. Beispiele;
Isomorphielemma; die von einer Formel
definierte Relation; Erfüllbarkeit; Allgemeingültigkeit;
Folgerungsbeziehung; Äquivalenz; Substitutionen (informal)
Mi, 12.12.12: Folien 200-206. Substitutionen; Beweis des Substitutionslemmas für Terme;
Beweis des Substitutionslemmas für Formeln; Umbenennen
gebundener Variablen; Negationsnormalform
Mo, 17.12.12: Folien 206-213. Äquivalenzen; Pränexe Normalform
Wiederholung
Logik der 1. Stufe; Ableitungen und Kalküle
Mi, 19.12.12: Folien 214-223. Abgeschlossene
Mengen in Kalkülen; Sequenzenkalkül für die Logik der ersten
Stufe
Mi, 9.1.13: Folien 230-238. Kompaktheitssatz;
Nichtdefinierbarkeit der endlichen Strukturen; Satz von
Löwenheim-Skolem; Nichtdefinierbarkeit der zusammenhängenden Graphen; Erfüllbarkeitsreduktionen;
Elimination von freien Variablen;
Mo, 14.1.13: Folien 239-240.
Elimination der Gleichheit; Elimination von Existenzquantoren (ohne Beweis)
Mi, 16.1.13: Folien 240-246. Elimination von Existenzquantoren(Beweis);
Skolem-Normalform; Klauselnormalform; Grundterme und Grundatome; Herbrandstrukturen;
Mo, 21.1.13: Folien 247-251. Satz
von Herbrand; Reduktion des prädikatenlogischen auf das
aussagenlogische Erfüllbarkeitsproblem
Mi, 23.1.13: Folien
252-260. Beweis des Reduktionssatzes; automatische
Theorembeweiser; Prädikatenlogische Resolution; Logikprogrammierung und die
Logik der 1.Stufe
Mo, 28.1.13: Folien 261-271. Nullestellige Relationen.
Übersetzung von Logikprogrammen in die Logik der
ersten Stufe; Modelltheoretische Charakterisierung der
Semantik von Logikprogrammen
Mi, 30.2.13: Folien 272-283.
minimale Herbrandmodelle; modelltheoretische
Sichtweise auf Anfragen; Semi-Entscheidbarkeit des
Allgemeingültigkeits und des Folgerungdproblems; Unentscheidbarkeit der Logik der 1.Stufe
Mo, 4.2.13: Folie 284.
Simulation von Turingmaschinen durch Logikprogramme; Beweis der Unentscheidbarkeit von FOLG
