|
Logik in der Informatik
Prof. Dr. Nicole Schweikardt |
|
Hier finden Sie (nach den Vorlesungen) Informationen zum Inhalt der einzelnen Vorlesungsstunden, Tipps zum Weiterlesen und gelegentlich ergänzende Bemerkungen.
Vorsicht: In der Vorlesung und der Übung werden viele wichtige Dinge (insbesondere Beweise, aber auch einiges andere) an der Tafel erklärt. Diese Dinge sind für die Veranstaltung "Logik und Datenbanken" wesentlich und daher auch dann prüfungsrelevant, wenn sie nicht in den hier erhältlichen pdf-Dateien der Folien enthalten sind.
Eröffnungsveranstaltung. Klärung von Organisatorischem (entlang der Webseite der Vorlesung). Kapitel 1: Einleitung. Kapitel 2: Das Relationale Modell - heute: Relationsschemata und Relationen
Material:
Folien 1-16
Weitere Lektüre:
Teil A von [AHV] und Abschnitte
19.1 und 19.2 des Artikels [SSS]
Abschluss von Kapitel 2: Das Relationale Modell - heute:
Datenbankschemata und Datenbank(instanz)en, Beispieldatenbank mit
Kinodaten, Anfragen und Anfragefunktionen,
generische Anfragefunktionen, Boolesche Anfragen, Datenkomplexität und kombinierte
Komplexität
Start mit Kapitel 3: Konjunktive Anfragen - heute: Syntax und Semantik von
regelbasierten konjunktiven Anfragen
Material:
Folien 17-38
Weitere Lektüre:
Teil A und Kapitel 4.1 und 4.2 von [AHV]
Weiter mit Kapitel 3: Konjunktive Anfragen - heute: der "active domain" von Datenbanken und Anfragen; Monotonie und Erfüllbarkeit regelbasierter konjunktiver Anfragen; Syntax und Semantik von Tableau-Anfragen
Material:
Folien 39-45,
Übungsblatt 1
Weitere Lektüre:
Teil A und Kapitel 4.1 und 4.2 von [AHV]
Weiter mit Kapitel 3: Konjunktive Anfragen - heute: Syntax und Semantik des konjunktiven Kalküls; eine Normalform für CQ; Äquivalenz der Ausdrucksstärke von Tableau-Anfragen, konjunktivem Kalkül und regelbasierten konjunktiven Anfragen; regelbasierte konjunktive Anfragen mit "="
Material:
Folien 46-61
Weitere Lektüre:
Teil A und Kapitel 4.1 und 4.2 von [AHV]
Weiter mit Kapitel 3: Konjunktive Anfragen - heute: regelbasierte konjunktive Programme; Auswertungskomplexität konjunktiver Anfragen: ein "naiver" Algorithmus zum Auswerten konjunktiver Anfragen; der Begriff der "Algorithmen mit Verzögerung f(k,n)"; Beginn des Beweises von Theorem 3.20 (Transformation eines Algorithmus zur Auswertung Boolescher Anfragen des konjunktiven Kalküls zu einem Algorithmus zur Auswertung beliebiger Anfragen des konjunktiven Kalküls, so dass die Verzögerung zwischen der Ausgabe zweier Ergebnis-Tupel O(k^3 n) ist)
Material:
Folien 61-70,
Übungsblatt 2
Weitere Lektüre:
Kapitel 4.3 von [AHV]
Weiter mit Kapitel 3: Konjunktive Anfragen - heute: Abschluss des Beweises von Theorem 3.20 (Transformation eines Algorithmus zur Auswertung Boolescher Anfragen des konjunktiven Kalküls zu einem Algorithmus zur Auswertung beliebiger Anfragen des konjunktiven Kalküls, so dass die Verzögerung zwischen der Ausgabe zweier Ergebnis-Tupel O(k^3 n) ist); NP, Polynomialzeit-Reduktionen und NP-Vollständigkeit; Nachweis der NP-Vollständigkeit des Auswertungsproblems (kombinierte Komplexität) für Boolesche regelbasierte konjunktive Anfragen (ein Satz von Chandra und Merlin)
Material:
Folien 70-77
Weitere Lektüre:
Kapitel 4.3 von [AHV];
die Originalarbeit [CM] von Chandra
und Merlin finden Sie hier
Weiter mit Kapitel 3: Konjunktive Anfragen - heute: Folgerung aus der NP-Vollständigkeit; SPC-Algebra und SPJR-Algebra: Syntax, Semantik und viele Beispiele
Material:
Folien 78-94,
Übungsblatt 3
Weitere Lektüre:
Kapitel 4.3, 4.4 und 4.5 von [AHV];
die Originalarbeit [CM] von Chandra
und Merlin finden
Sie hier;
eine Einführung [G] in die Parametrische Komplexität für
Datenbanktheoretiker_innen ist
hier erhältlich.
Weiter mit Kapitel 3: Konjunktive Anfragen - heute: Nachweis der Äquivalenz der Ausdrucksstärke von SPC-Algebra und SPJR-Algebra; Nachweis der Äquivalenz zwischen SPC-Algebra, SPJR-Algebra, Tableau-Anfragen, regelbasierten konjunktiven Anfragen und Anfragen des konjunktiven Kalküls; Vorbemerkungen zum Thema Optimierung; Definition des Erfüllbarkeitsproblems, des Äquivalenzproblems, des Query Containment Problems
Material:
Folien 95-102
Weitere Lektüre:
Kapitel 4.4, 4.5 und 6.2 von [AHV]
Weiter mit Kapitel 3: Konjunktive Anfragen - heute: Einführung der Begriffe "Substitution", "Homomorphismus" (für Tableau-Anfragen) und "Kanonische Datenbanken"; den Homomorphismussatz bewiesen
Material:
Folien 103-107
Weitere Lektüre:
Kapitel 6.2-6.4 von [AHV];
die Originalarbeit [CM] von Chandra
und Merlin finden Sie hier
Weiter mit Kapitel 3: Konjunktive Anfragen - heute: NP-Vollständigkeit des Query Containment Problems für Tableau-Anfragen nachgewiesen; Minimierung von Tableau-Anfragen; Greedy-Algorithmus zur Minimierung von Tableau-Anfragen (inkl. Korrektheitsbeweis)
Material:
Folien 107-109
Weitere Lektüre:
Kapitel 6.2-6.4 von [AHV];
die Originalarbeit [CM] von Chandra
und Merlin finden Sie hier
Weiter mit Kapitel 3: Konjunktive Anfragen - heute: ein Beispiel zur Verwendung der Tableau-Minimierung zur Optimierung von SPJR-Anfragen; azyklische konjunktive Anfragen, Join-Bäume, Semijoin-Anfragen, ein effizienter Algorithmus zur Auswertung von Semijoin-Anfragen
Material:
Folien 110-116,
Übungsblatt 4
Weitere Lektüre:
Kapitel 6.2 und 6.4 von [AHV]
Weiter mit Kapitel 3: Konjunktive Anfragen - heute: die Äquivalenz von Booleschen Semijoin-Anfragen und azyklischen regelbasierten Booleschen Anfragen
Material:
Folien 117
Weitere Lektüre:
Kapitel 6.2 und 6.4 von [AHV]
Weiter mit Kapitel 3: Konjunktive Anfragen - heute: ein Algorithmus zum Test auf Azyklizität und zum Erzeugen von Join-Bäumen (inkl. Korrektheitsbeweis); der Satz von Yannakakis, der besagt, dass das Auswertungsproblem für azyklische konjunktive Anfragen (kombinierte Komplexität) in Polynomialzeit gelöst werden kann; die Komplexitätsklasse LOGCFL
Material:
Folien 118-121,
Übungsblatt 5
Weitere Lektüre:
Kapitel 6.2 und 6.4 von [AHV].
Die Originalarbeit [Y] von Yannakakis.
Einen Überblick über
Verallgemeinerungen des Begriffs der azyklischen Anfragen gibt die
Arbeit [Sca] von Scarcello.
Abschluss von Kapitel 3: Konjunktive Anfragen - heute: das konjunktive Guarded Fragment GF(CQ) eingeführt und gezeigt, dass mit Sätzen von GF(CQ) genau dieselben Booleschen Anfragen beschrieben werden können wie mit Booleschen Semijoin-Anfragen bzw. mit azyklischen Booleschen regelbasierten Anfragen; kurzer Überblick über die Multimengen-Semantik regelbasierter konjunktiver Anfragen, inkl. Überblick über Forschungsergebnisse und offene Forschungsfragen
Material:
Folien 122-132
Weitere Lektüre:
Kapitel 6.2 und 6.4 von [AHV].
Start mit Kapitel 4: Datalog - heute: einführendes Beispiel; Syntax von Datalog; der "immediate consequence-Operator" TP und der "Stufen-Operator" SP; die Fixpunkt-Semantik von Datalog; ein Algorithmus zum Auswerten von Datalog-Anfragen (dessen Datenkomplexität in Polynomialzeit liegt); Modellbasierte Semantik von Datalog und der Satz von Knaster und Tarski
Material:
Folien 133-147,
Übungsblatt 6
Weitere Lektüre:
Umfassende Informationen zum Thema Datalog finden sich in Teil D
von [AHV] und in dem Überblicksartikel
[Datalog] von Dantsin, Eiter,
Gottlob und Voronkov
Weiter mit Kapitel 4: Datalog - heute: Beweisbasierte Semantik von Datalog, Fakten und Beweisbäume; Monotonie von Datalog-Anfragen Q und deren Abschluss unter adom(Q)-Homomorphismen; Konstruktion eines Datalog-Programms PM,k, das bei Eingabe einer Datenbank Iw, die ein Wort w repräsentiert, die ersten |w|k-1 Schritte des Laufs der Turingmaschine M bei Eingabe w simuliert: Beginn des Beweises
Material:
Folien 148-155
Weitere Lektüre:
Umfassende Informationen zum Thema Datalog finden sich in Teil D
von [AHV] und in dem Überblicksartikel
[Datalog] von Dantsin, Eiter,
Gottlob und Voronkov; in letzterem ist auch ein Beweis des Satzes von
Immerman und Vardi über die Komplexität des Auswertungsproblems für
Datalog-Anfragen zu finden.
Weiter mit Kapitel 4: Datalog - heute: Konstruktion eines Datalog-Programms PM,k, das bei Eingabe einer Datenbank Iw, die ein Wort w repräsentiert, die ersten |w|k-1 Schritte des Laufs der Turingmaschine M bei Eingabe w simuliert: Weiterführung des Beweises; Formulierung eines Satzes von Immerman und Vardi, der besagt, dass das Auswertungsproblem für Datalog-Anfragen bzgl. kombinierter Komplexität EXPTIME-vollständig und bzgl. Datenkomplexität PTIME-vollständig ist
Material:
Folien 155-156,
handschriftliche Notizen zum
Beweis von Satz 4.13 (Datalog zur Simulation von Turingmaschinen),
Übungsblatt 7
Weitere Lektüre:
Umfassende Informationen zum Thema Datalog finden sich in Teil D
von [AHV] und in dem Überblicksartikel
[Datalog] von Dantsin, Eiter,
Gottlob und Voronkov; in letzterem ist auch ein Beweis des Satzes von
Immerman und Vardi über die Komplexität des Auswertungsproblems für
Datalog-Anfragen zu finden. Grundlegende Informationen zu
logspace-Reduktionen und zur PTIME-Vollständigkeit finden sich z.B. in
Kapitel 8 "Reductions and Completeness" des Buchs [P].
Erster Zwischentest
Weiter mit Kapitel 4: Datalog - heute:
Konstruktion eines Datalog-Programms PM,k, das bei Eingabe
einer
Datenbank Iw, die ein Wort w repräsentiert, die ersten
|w|k-1 Schritte des Laufs der Turingmaschine M bei
Eingabe w simuliert: Abschluss des Beweises;
das Erfüllbarkeitsproblem für Datalog-Anfragen;
das Query Containment Problem (QCP) für Datalog-Anfragen;
Beginn des Beweises der Unentscheidbarkeit des QCP für Datalog-Anfragen
Material:
Folien 155-158
Weitere Lektüre:
Umfassende Informationen zum Thema Datalog finden sich in Teil D
von [AHV] und in dem Überblicksartikel
[Datalog] von Dantsin, Eiter,
Gottlob und Voronkov
Weiter mit Kapitel 4: Datalog - heute: Abschluss des Beweises der Unentscheidbarkeit des QCP für Datalog-Anfragen; Beschränktheit von Datalog-Programmen; Idee zum Beweis der Unentscheidbarkeit der Beschränktheit von Datalog-Programmen
Material:
Folien 158-161,
Übungsblatt 8
Weitere Lektüre:
Umfassende Informationen zum Thema Datalog finden sich in Teil D
von [AHV] und in dem Überblicksartikel
[Datalog] von Dantsin, Eiter,
Gottlob und Voronkov
Weiter mit Kapitel 4: Datalog - heute: nicht-rekursives Datalog (nr-Datalog), der Abhängigkeitsgraph eines Datalog-Programms, Charakterisierung der Ausdrucksstärke von nr-Datalog via SPCU-Algebra und positiv existentiellen Kalkül
Material:
Folien 162-166,
Übungsblatt 9
Weitere Lektüre:
Umfassende Informationen zum Thema Datalog finden sich in Teil D
von [AHV] und in dem Überblicksartikel
[Datalog] von Dantsin, Eiter,
Gottlob und Voronkov
Abschluss von Kapitel 4: Datalog - heute:
Datalog mit Negation: semipositives Datalog mit Negation,
stratifiziertes Datalog mit Negation, nicht-rekursives Datalog mit Negation
Beginn mit Kapitel 5: Funktionale Abhängigkeiten - heute:
Einführung ins Thema
Material:
Folien 167-185
Weitere Lektüre:
Kapitel 8.1 und 8.2 von [AHV]
Umfassende Informationen zum Thema Datalog finden sich in Teil D
von [AHV] und in dem Überblicksartikel
[Datalog] von Dantsin, Eiter,
Gottlob und Voronkov
Weiter mit Kapitel 5: Funktionale Abhängigkeiten - heute: Grundbegriffe zum Thema "funktionale Abhängigkeiten" und FD-Mengen; verlustfreie Joins (inkl. Beweis von Proposition 6.2); Beginn des Abschnitts über "The Chase - die Verfolgungsjagd": ein Beispiel zur Minimierung von Tableau-Anfragen unter Berücksichtigung von funktionalen Abhängigkeiten; Äquivalenz und Query Containment bzgl. einer FD-Menge F; die FD-Regel; Nachweis, dass das Anwenden der FD-Regel Äquivalenz bzgl. einer FD-Menge F erhält (Proposition 5.6)
Material:
Folien 186-192,
Übungsblatt 10
Weitere Lektüre:
Kapitel 8.4 von [AHV]
Weiter mit Kapitel 5: Funktionale Abhängigkeiten - heute: Verfolgungssequenzen und deren Eigenschaften; ein Polynomialzeit-Algorithmus zur Berechnung von chase(T,t,F); Algorithmen für Query Containment und Äquivalenz von konjunktiven Anfragen relativ zu einer FD-Menge, Minimierung von konjunktiven Anfragen relativ zu einer FD-Menge; Implikation von funktionalen Abhängigkeiten
Material:
Folien 193-201
Weitere Lektüre:
Kapitel 8.4 und 8.2 von [AHV]
Weiter mit Kapitel 5: Funktionale Abhängigkeiten - heute: ein Polynomialzeit-Algorithmus zum Entscheiden, ob eine FD f aus einer FD-Menge F folgt (Satz 5.17); der Armstrong-Kalkül
Material:
Folien 201-206;
Übungsblatt 11
Weitere Lektüre:
Kapitel 8.2 von [AHV]
Abschluss von Kapitel 5: Funktionale Abhängigkeiten - heute:
Nachweis der Vollständigkeit des Armstrong-Kalküls
Start mit Kapitel 6: Relationale Algebra - heute:
Syntax und Semantik der relationalen Algebra;
Beispiele für Anfragen der relationalen Algebra;
Vergleich der Ausdrucksstärke von SPC-Algebra, SPCU-Algebra und relationaler Algebra;
(Nicht-)Redundanz einzelner Operatoren der relationalen Algebra;
Theta-Joins und Semijoins
Material:
Folien 206-213
Weitere Lektüre:
Kapitel 5.1 und 6.1 von [AHV]
Abschluss von Kapitel 6: Relationale Algebra - heute: Anfrageauswertung und heuristische Optimierung; Join-Reihenfolge, SIP-Graph und SIP-Strategien
Material:
Folien 214-239,
Übungsblatt 12
Weitere Lektüre:
Kapitel 6.1 von [AHV]
Start mit Kapitel 7: Relationenkalkül - heute: Relationenkalkül mit natürlicher Semantik, Relationenkalkül mit Active Domain Semantik und bereichsunabhängigen Relationenkalkül eingeführt und an Beispielen illustriert; Erster Teil des Beweises, dass die relationale Algebra, der Relationenkalkül mit Active Domain Semantik und der bereichsunabhängige Relationenkalkül dieselbe Ausdrucksstärke haben
Material:
Folien 240-253
Weitere Lektüre:
Kapitel 5.3 von [AHV];
Weiter mit Kapitel 7: Relationenkalkül - heute: Abschluss des Beweises, dass die relationale Algebra, der Relationenkalkül mit Active Domain Semantik und der bereichsunabhängige Relationenkalkül dieselbe Ausdrucksstärke haben; den Satz von Trakhtenbrot zitiert und benutzt, um die Beweisidee dafür anzugeben, dass es keinen Algorithmus gibt, der bei Eingabe einer Anfrage des Relationenkalküls entscheidet, ob die Anfrage bereichsunabhängig ist
Material:
Folien 253-256
Weitere Lektüre:
Kapitel 5.3 von [AHV];
zum Satz von Trakhtenbrot siehe Kapitel 9.1 von [L]
Weiter mit Kapitel 7: Relationenkalkül - heute: detaillierter Beweis (unter Verwendung des Satzes von Trakhtenbrot) dafür, dass es keinen Algorithmus gibt, der bei Eingabe einer Anfrage des Relationenkalküls entscheidet, ob die Anfrage bereichsunabhängig ist; den sicheren Relationenkalkül CALCsr eingeführt und an Beispielen illustriert
Material:
Folien 256-263,
Übungsblatt 13
Weitere Lektüre:
Kapitel 5.4 von [AHV]
Weiter mit Kapitel 7: Relationenkalkül - heute: nachgewiesen, dass der sichere Relationenkalkül CALCsr bereichsunabhängig ist und genau dieselbe Ausdrucksstärke wie die relationale Algebra hat;
Material:
Folien 264-265
Weitere Lektüre:
Kapitel 5.4 und 6.3 von [AHV]
Abschluss von Kapitel 7: Relationenkalkül - heute: die Unentscheidbarkeit der statischen Analyse für relational vollständige Anfragesprachen nachgewiesen; Beweis des Satzes von Chandra und Merlin, der besagt, dass das Auswertungsproblem für Boolesche Anfragen des Relationenkalküls PSPACE-vollständig ist (bzgl. der kombinierten Komplexität) die Komplexitätsklasse AC° und die Datenkomplexität des Auswertungsproblems des Relationenkalküls betrachtet; Beweisidee für den Satz von Immerman, der besagt, dass die Datenkomplexität von Booleschen Anfragen des Relationenkalküls in AC° liegt. Kapitel 8: Zusammenfassung und Ausblick, Abschluss der Veranstaltung, Hinweise zur Vorbereitung auf eine mündliche Modulabschlussprüfung
Material:
Folien 266-273 und 278-284
Weitere Lektüre:
Kapitel 5.4 und 6.3 von [AHV]