|
Logik in der Informatik
Prof. Dr. Nicole Schweikardt |
|
In diesem Logbuch finden Sie (nach den Vorlesungen) Informationen zum Inhalt der einzelnen Vorlesungsstunden, die entsprechenden Teile des Skripts und gelegentlich auch Korrekturen und sonstige ergänzende Bemerkungen.
Am Dienstag, dem 13.10.26, findet die Eröffnungsvorlesung statt.
Kapitel 1: Einführung ins Thema "Logik in der Informatik" — heute:
Paradoxien, Syllogismen, Anwendungen der Logik in der
Informatik, Logik-Programmierung und Prolog; Lernziele des Moduls, Semesterausblick, Literatur
Organisatorisches (entlang der Webseite der Vorlesung).
Material:
Skript Seiten 1-20
Weitere Lektüre:
Kapitel 1 und 2.A in [KK],
Einleitung und Kapitel 1.1 in [S],
Vorwort und Kapitel 1.1, 1.5 und 2.1
in [B],
"Indroduction" der beiden Bücher [SS] und [BBS].
Eine Vorabversion des in der Vorlesung zitierten Artikel "On the unusual effectiveness of
logic in computer science" von Halpern, Harper, Immerman, Kolaitis, Vardi
und Vianu (Bulletin of Symbolic Logic 7(2):213-236 (2001)) finden
Sie hier.
Start mit Kapitel 2: Aussagenlogik — heute: Einführung und Beispiele, Syntax und Semantik der Aussagenlogik, rekursive Definitionen über Formeln, ein Beispiel zur Auswertung einer Formel
Material:
Skript Seiten 21-31 (bis zum Ende von Folie 50)
Weitere Lektüre:
Kapitel 1 und 2.A in [KK],
Einleitung und Kapitel 1.1 in [S],
Kapitel 2.1 und 2.2 in [B].
Weiter mit Kapitel 2: Aussagenlogik - heute: Modelle, das Koinzidenzlemma, Vereinbarungen und Notationen, Wahrheitstafeln, ein Logikrätsel, computerlesbare Darstellung von Formeln; Demo des Formelcheckers für die Aussagenlogik "snippets-of-logic"; Auflösung des Rätsels zur Geburtstagsfeier (Beispiel 2.1); Erfüllbarkeit, Allgemeingültigkeit, Folgerungsbeziehung
Material:
Skript Seiten 32-43 (bis inkl. Folie 73),
Formelchecker für die Aussagenlogik: snippets-of-logic
Weitere Lektüre:
Kapitel 1 und 2.A in [KK],
Kapitel 1.1 und 1.2 in [S],
Kapitel 2.2 in [B].
Weiter mit Kapitel 2: Aussagenlogik - heute: Modus Ponens; Zusammenhänge zwischen Allgemeingültigkeit, Erfüllbarkeit und Folgerungsbeziehung; aussagenlogische Modellierung am Beispiel von Sudokus; kurze Info zur aussagenlogischen Modellierung am Beispiel der automatischen Hardwareverifikation (Details hierzu finden sich im Vorlesungsskript); Äquivalenz von Formeln und Formelmengen; fundamentale Äquivalenzen
Material:
Skript Seiten 43-53 (bis inkl. Folie 86)
Weitere Lektüre:
Kapitel 2.A in [KK],
Kapitel 1.1 und 1.2 in [S],
Kapitel 2.4.1 und 2.5 in [B].
Weiter mit Kapitel 2: Aussagenlogik - heute: Definition des Begriffs duale Formel; der Dualitätssatz der Aussagenlogik; boolesche Funktionen und die funktionale Vollständigkeit der Aussagenlogik
Material:
Skript Seiten 53-61 (bis zum Anfang von Folie 99)
Weitere Lektüre:
Kapitel 2.A in [KK],
Kapitel 1.2 und 1.4 in [S],
Kapitel 2.6 und 2.8 in [B].
Weiter mit Kapitel 2: Aussagenlogik - heute: Adäquatheit von Mengen von Junktoren und Konstanten; detaillierter Beweis der Adäquatheit von {¬,∨} (formuliert als "Satz 1"); detaillierter Beweis für die Adäquatheit von {¬,∧} (formuliert als "Satz 2"); detaillierter Beweis für die Adäquatheit von {0, →} (formuliert als "Satz 3"); Beweisidee für die Nicht-Adäquatheit von {∨, ∧, →}; weitere Junktoren: exklusives Oder, der Mehrheitsjunktor und der Sheffer-Strich (NAND-Gatter); Beweisidee für die Adäquatheit des Sheffer-Strichs; Negationsnormalform (NNF): Beispiele, ein Algorithmus zur Transformation in NNF, Satz zur Existenz von äquivalenten Formeln in NNF
Material:
Skript Seiten 61-67 (bis inkl. Folie 108)
Weitere Lektüre:
Kapitel 2.A und 2.B in [KK],
Kapitel 1.4 und 1.5 in [S],
Kapitel 2.8 und 2.10 in [B].
Weiter mit Kapitel 2: Aussagenlogik - heute: Disjunktive Normalform (DNF); Konjunktive Normalform (KNF); Beispiele und Algorithmen zur Transformation in NNF, DNF und KNF; eine kurze Formel in KNF, so dass jede hierzu äquivalente DNF-Formel exponentiell länger ist; Formulierung und Anfang des Beweises des Endlichkeitssatzes
Material:
Skript Seiten 68-75 (bis direkt vor den Beweis von Behauptung 3)
Weitere Lektüre:
Kapitel 2.A und 2.B in [KK],
Kapitel 1.4 und 1.5 in [S],
Kapitel 2.8 und 2.10 in [B].
Weiter mit Kapitel 2: Aussagenlogik - heute: Abschluss des Beweises des Endlichkeitssatzes; eine Anwendung des Endlichkeitssatzes: Nachweis, dass ein unendlicher Graph genau dann k-färbbar ist, wenn jeder endliche Subgraph k-färbbar ist; einführendes Beispiel zum Thema Resolution
Material:
Skript Seiten 75-79 (bis inkl. Folie 121)
Weitere Lektüre:
Kapitel 2.B in [KK],
Kapitel 1.5 in [S],
Kapitel 2.10 in [B].
Weiter mit Kapitel 2: Aussagenlogik - heute: Tseitin-Verfahren zur effizienten Umwandlung beliebiger Formeln in erfüllbarkeitsäquivalente KNF-Formeln; Repräsentation disjunktiver Klauseln durch endliche Mengen von Literalen; Repräsentation von KNF-Formeln durch endliche Klauselmengen; der Begriff einer Resolvente zweier Klauseln; das Resolutionslemma (inkl. Beweis); Resolutionsableitungen und Resolutionswiderlegungen; Beispiel für eine Resolutionswiderlegung; Formulierung des Satzes über die Korrektheit und Vollständigkeit der Resolution (d. h. eine Klauselmenge besitzt genau dann eine Resolutionswiderlegung, wenn sie unerfüllbar ist) — heute noch ohne Beweis; Vorsicht beim Anwenden der Resolutionsregel
Material:
Skript Seiten 79-86 und 89 (bis inkl. Folie 135)
Weitere Lektüre:
Kapitel 2.B in [KK],
Kapitel 1.5 in [S],
Kapitel 2.10 in [B].