|
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 14.10.25, fand 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, Modelle, das Koinzidenzlemma, Vereinbarungen und Notationen
Material:
Skript Seiten 21-33 (bis zum Ende von Folie 53)
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: weitere 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, Modus Ponens; Zusammenhänge zwischen Allgemeingültigkeit, Erfüllbarkeit und Folgerungsbeziehung
Material:
Skript Seiten 33-45 (bis inkl. Folie 76),
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: 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; Definition des Begriffs duale Formel und Formulierung des Dualitätssatzes
Material:
Skript Seiten 45-55 (bis inkl. Folie 91)
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: Beweise per Induktion über den Aufbau von Formeln; Beweis des Dualitätssatzes der Aussagenlogik; boolesche Funktionen und die funktionale Vollständigkeit der Aussagenlogik; Adäquatheit von Mengen von Junktoren und Konstanten; detaillierter Beweis der Adäquatheit von {¬,∧} (formuliert als "Lemma 1")
Material:
Skript Seiten 55-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: detaillierter Beweis für die Adäquatheit von {¬,∨} (formuliert als "Lemma 2"); detaillierter Beweis für die Adäquatheit von {0, →} (formuliert als "Lemma 3"); Beweisidee für die Nicht-Adäquatheit von {∨, ∧, →} (formuliert als "Lemma 4"); 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; Disjunktive Normalform (DNF)
Material:
Skript Seiten 61-68 (bis inkl. Folie 110)
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: 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 Beweis des Endlichkeitssatzes
Material:
Skript Seiten 68-75
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: 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; 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
Material:
Skript Seiten 75-83 (bis inkl. Folie 128)
Weitere Lektüre:
Kapitel 2.B in [KK],
Kapitel 1.5 in [S],
Kapitel 2.10 in [B].
Weiter mit Kapitel 2: Aussagenlogik - heute: das Resolutionslemma (inkl. Beweis); Resolutionsableitungen und Resolutionswiderlegungen; Beispiel für eine Resolutionswiderlegung; Beweis des Satzes über die Korrektheit und Vollständigkeit der Resolution (d. h. eine Klauselmenge besitzt genau dann eine Resolutionswiderlegung, wenn sie unerfüllbar ist); Vorsicht beim Anwenden der Resolutionsregel; der Satz von Haken (ohne Beweis); Algorithmen zur Lösung des (NP-vollständigen) aussagenlogischen Erfüllbarkeitsproblems: der Wahrheitstafelalgorithmus, der Resolutionsalgorithmus, der DPLL-Algorithmus
Material:
Skript Seiten 83-94 (bis inkl. Folie 144)
Weitere Lektüre:
Kapitel 2.B in [KK],
Kapitel 1.5 in [S],
Kapitel 2.10 in [B].
Weiter mit Kapitel 2: Aussagenlogik - heute: Wiederholung der in den letzten 3 Vorlesungen behandelten Inhalte, insbes. zum Endlichkeitssatz und desssen Anwendungen sowie zum Thema "Resolution"; Details zum DPLL-Algorithmus (inkl. Beispiel)
Material:
Skript Seiten 93-97 (bis zum Ende von Folie 145)
Weitere Lektüre:
Kapitel 2.B in [KK],
Kapitel 1.5 in [S],
Kapitel 2.10 in [B].
Die SAT Competition ist ein
jährlich stattfindender internationaler Wettbewerb, bei dem effiziente
Implementierungen von Algorithmen zur Lösung des SAT-Problems
gegeneinander antreten. Mehr Details finden Sie auf der Webseite der
SAT Competition 2014.
Im Jahr 2014 fanden im Rahmen des Vienna Summer of Logic
auch die FLoC Olympic Games 2014
statt, in die die SAT Competition 2014 eingebettet war.
Ein sehr guter Überblick über den Stand der Forschung zum Thema
"SAT-Solver" findet sich beispielsweise in der
Dissertation Towards Next Generation Sequential and Parallel
SAT Solvers von
Dr. Norbert
Manthey (TU Dresden, 2014).
Abschluss von Kapitel 2: Aussagenlogik - heute: Hornklauseln und Hornformeln; der Streichungsalgorithmus (ein effizienter Erfüllbarkeitsalgorithmus für Hornformeln): Algorithmus, zwei Beispiel-Läufe, Laufzeitanalyse und Korrektheitsbeweis
Material:
Skript Seiten 97-104 (bis zum Ende von Kapitel 2)
Weitere Lektüre:
Kapitel 1.3 in [S],
Kapitel 2.11 in [B].
Start mit Kapitel 3: Logik erster Stufe - heute: Signaturen, Strukturen, Beispiele für Signaturen und Strukturen, Eigenschaften 2-stelliger Relationen, Äquivalenzrelationen, Ordnungen, arithmetische Strukturen, Wörter als Strukturen, relationale Datenbanken als Strukturen; Restriktionen und Expansionen; Isomorphie
Material:
Skript Seiten 105-114 (bis inkl. Folie 174)
Weitere Lektüre:
Kapitel I und Kapitel III.1 in [EFT].
Einen Überblick über die Rolle der Logik in der Informatik gibt der 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)), den
Sie hier
finden.
Einen Überblick über die Geschichte der logischen Grundlagen der
Mathematik gibt der Comic Logicomix.
Weiter mit Kapitel 3: Logik erster Stufe - heute: Beispiele für Isomorphismen; Variablen und Terme der Logik erster Stufe, Belegungen, σ-Interpretationen, Semantik von σ-Termen; Vergleich zwischen Aussagenlogik und Logik erster Stufe; Syntax der Logik erster Stufe; Beispiele zur Syntax der Logik erster Stufe
Material:
Skript Seiten 114-123 (bis zum Ende von Folie 192)
Weitere Lektüre:
Kapitel I und Kapitel III.1 in [EFT].
Einen Überblick über die Rolle der Logik in der Informatik gibt der 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)), den
Sie hier
finden.
Einen Überblick über die Geschichte der logischen Grundlagen der
Mathematik gibt der Comic Logicomix.
Weiter mit Kapitel 3: Logik erster Stufe - heute: Beispiele zur Semantik der Logik erster Stufe; formale Definition der Semantik der Logik erster Stufe; die Modellbeziehung; Subformeln, Subterme und Syntaxbäume; generelle Form von Beweisen per Induktion über den Aufbau von Termen und Formeln; Formulierung und Beginn des Beweises des Isomorphielemmas der Logik erster Stufe (heute: Beweis für Terme)
Material:
Skript Seiten 123-134 (bis zum Ende von Folie 217)
Weitere Lektüre:
Kapitel III.1 und Kapitel II.1-3 in [EFT].
Weiter mit Kapitel 3: Logik erster Stufe - heute: Abschluss des Beweises des Isomorphielemmas der Logik erster Stufe (heute: für Formeln); das Koinzidenzlemma der Logik erster Stufe; Sätze der Logik erster Stufe; Modellklassen und Definierbarkeit (bzw. Axiomatisierbarkeit) von Klassen von Strukturen; Beispiele für Formeln der Logik erster Stufe in verschiedenen Anwendungsbereichen: lineare Ordnungen, Arithmetik, Worte
Material:
Skript Seiten 133-144 (bis inkl. Folie 232)
Weitere Lektüre:
Kapitel II.1-3 und Kapitel III.2-3
in [EFT];
Chapter 5.1-5.7 in [B]
Kapitel 4.A in [KK];
Kapitel 2.1 und 2.2 in [S]
Weiter mit Kapitel 3: Logik erster Stufe - heute: Beispiele für Formeln der Logik erster Stufe im Anwendungsbereich "Datenbanken"; eine andere Sicht auf die Semantik der Logik erster Stufe: die von einer Formel in einer Struktur definierte n-stellige Relation; rekursive Beschreibung dieser Relation, die zu einem Algorithmus führt, der das Auswertungsproblem für FO löst; Äquivalenz von Formeln der Logik erster Stufe; Übertragung von aussagenlogischen Äquivalenzen auf Äquivalenz von Formeln der Logik erster Stufe (Lemma 3.43); Zusammenspiel zwischen Quantoren und Negationen; das Ersetzungslemma (inkl. Folgerungen daraus)
Material:
Skript Seiten 144-154 (bis inkl. Folie 251)
Weitere Lektüre:
Kapitel II.4-5 und Kapitel III.4-5
in [EFT];
Chapter 5.1-5.7 in [B]
Kapitel 4.A in [KK];
Kapitel 2.1 und 2.2 in [S]