Mi, 16.10.13: Folien 1-30. Paradoxien; Syllogismen;
Anwendungen der Logik in der Informatik; Syntax der Aussagenlogik; Semantik(Vorbereitung); Semantik der
Aussagenlogik
Mo, 21.10.13: Folien 31-51. Rekursive Definitionen über Formeln;
Koinzidenzlemma; Wahrheitstafeln; Erfüllbarkeit;
Allgemeingültigkeit; Folgerungsbeziehung; aussagenlogische
Modellierung von Sudoku; Anwendung
Schaltkreisverifikation
Mo, 28.10.13: Folien 62-68. funktionale Vollständigkeit;
Adäquatheit Beweis des Stazes über
die funktionale Vollständigkeit; Adäquatheit und neue Junktoren
Mi, 30.10.13: Folien 69-80. Negationsnormalform; konjunktive und disjunktive Normalform;
Kompaktheitssatz; Beweis des Kompaktheitssatzes
Mo, 4.11.13: Folien 81-87. Beweis des Kompaktheitssatzes (Fortsetzung); Anwendung auf Färbbarkeit unendlicher
Graphen; Beweis des Satzes über die Färbbarkeit von unendlichen Graphen;
Umwandlung in erfüllbarkeitsäquivalente KNF in
Linearzeit; Resolventen;
Resolutionslemma
Mi, 6.11.13: Folien 88-98. Resolutionswiderlegungen; Korrektheit und
Vollständigkeit der ResolutionKomplexität des
aussagenlogischen Erfüllbarkeitsproblems;
Erfüllbarkeitsalgorithmen, insbesondere DP-Algorithmus
Mo, 11.11.13: Folien 99-105.
Beispiel für einen Durchlauf des
DP-Algorithmus; Hornformeln; Streichungsalgorithmus; Beispiele; Korrektheit des Streichungsalgorithmus (ohne Beweis);
Beweis des Satzes über die Korrektheit des Streichungsalgorithmus
Mi, 13.11.13: Folien 106 -120. Beweis des Satzes über die Korrektheit des Streichungsalgorithmus (Fortsetzung);
Einführung in die
Logikprogrammierung und Prolog; Fakten; Anfragen; Regeln;
Beispielprogramme; Terme; Substitutionen; Grundterme
Ableitungen
Mo, 18.11.13: Folien 121-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 und Vollständigkeit des einfachen Interpreters (Induktionsanfang für (1) => (2))
Mi, 20.11.13: Folien 129-134. Beweis der Korrektheit und Vollständigkeit des
einfachen Interpreters (Fortsetzung); Unifikation; allgemeinste
Unifikatoren; Unifikationsalgorithmus; Beispiele zum
Unifikationsalgorithmus
Mo, 25.11.13: Folien 135-144.
Interpreter für Logikprogramme mit
Unifikation; Interpreter für reines Prolog; nichtterminierende
Prologberechnungen;
Suchbäume; Cut
Mi, 27.11.13: Folien 145-156. Suchbäume (Fortsetzung); Unifikation in
Prolog; Symbolmengen; Strukturen; Beispiele von Strukturen
Mo, 2.12.13: Folien 156-168. Beispiele von Strukturen (Fortsetzung); Strukturen aus
Logikprogrammen; Restriktionen und Expansionen; Isomorphie; Syntax der Logik der 1. Stufe
Mi, 4.12.13: Folien 169-178.
Freie
Variablen; Belegungen und Interpretationen; Semantik der Logik
der 1. Stufe; Koinzidenzlemma
Mi, 11.12.13: Folien 183-201. Beispiele (Fortsetzung); Isomorphielemma; die von einer Formel
definierte Relation; Erfüllbarkeit; Allgemeingültigkeit;
Folgerungsbeziehung; Äquivalenz; Substitutionen (informal); Substitutionen;
Beweis des Substitutionslemmas für Terme
