|
Logik in der Informatik
Prof. Dr. Nicole Schweikardt |
|
Wintersemester 2023/24
Dozent:in: Prof. Dr. Nicole Schweikardt und Dr. André Frochaux
In diesem Logbuch werden regelmäßig Informationen bereit gestellt. 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 "Einführung in die Datenbanktheorie" wesentlich und daher auch dann prüfungsrelevant, wenn sie nicht in den online erhältlichen Materialien 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, Datenbankschemata und Datenbank(instanz)en, Beispieldatenbank mit Kinodaten
Material:
Vorlesungsskript, Seiten 1-17 (bis inkl. Folie 21)
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:
benannte vs. unbenannte Perspektive, 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, viele Beispiele, der "active domain" von Datenbanken und Anfragen
Material:
Vorlesungsskript, Seiten 17-28 (bis inkl. Folie 40)
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; Syntax und Semantik des konjunktiven Kalküls; eine Normalform für CQ; Beispiele für Anfragen und Beispiele zur Übersetzung zwischen Tableau-Anfragen, Anfragen des konjunktiven Kalküls und regelbasierten konjunktiven Anfragen
Material:
Vorlesungsskript, Seiten 29-38 (bis inkl. Folie 54)
Weitere Lektüre:
Teil A und Kapitel 4.1 und 4.2 von [AHV]
Weiter mit Kapitel 3: Konjunktive Anfragen - heute: Korrektur der Definition von Syntax und Semantik des konjunktiven Kalküls; Beweis der Äquivalenz der Ausdrucksstärke von Tableau-Anfragen, konjunktivem Kalkül und regelbasierten konjunktiven Anfragen; regelbasierte konjunktive Anfragen mit "="
Material:
Vorlesungsskript, Seiten 38-44
Weitere Lektüre:
Kapitel 4.3 von [AHV]
Weiter mit Kapitel 3: Konjunktive Anfragen - heute: regelbasierte konjunktive Programme; Auswertungskomplexität konjunktiver Anfragen: das Auswertungsproblem für CQ (kombinierte Komplexität) und die Größe von Anfragen und Datenbanken; ein "naiver" Algorithmus zum Auswerten konjunktiver Anfragen; der Begriff der "Algorithmen mit Taktung 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 Taktung zwischen der Ausgabe zweier Ergebnis-Tupel O(k^3 n log n) ist)
Material:
Vorlesungsskript, Seiten 44-50
Weitere Lektüre:
Kapitel 4.3 von [AHV]
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 Taktung zwischen der Ausgabe zweier Ergebnis-Tupel O(k^3 n) ist) — algorithmische Technik: flashlight search; Wiederholung von Grundbegriffen zur Komplexitätsklasse NP und dem Begriff der NP-Vollständigkeit
Material:
Vorlesungsskript, Seiten 49-54
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: Wiederholung weiterer Grundbegriffe zur Komplexitätsklasse 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); Folgerung aus der NP-Vollständigkeit; Einführung zum Thema SPC-Algebra und SPJR-Algebra
Material:
Vorlesungsskript, Seiten 54-61 (bis inkl. Folie 81)
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 Parametrisierte Komplexität für
Datenbanktheoretiker*innen ist
hier erhältlich.
Weiter mit Kapitel 3: Konjunktive Anfragen - heute: SPC-Algebra und SPJR-Algebra: Syntax, Semantik und viele Beispiele; Nachweis der Äquivalenz der Ausdrucksstärke von SPC-Algebra und SPJR-Algebra; Satz über die Äquivalenz zwischen SPC-Algebra, SPJR-Algebra, Tableau-Anfragen, regelbasierten konjunktiven Anfragen und Anfragen des konjunktiven Kalküls (inkl. Beweisidee)
Material:
Vorlesungsskript, Seiten 61-73 (bis inkl. Folie 100)
Weitere Lektüre:
Kapitel 4.4, 4.5 und 6.2 von [AHV]
Weiter mit Kapitel 3: Konjunktive Anfragen - heute: Beweis zum Satz über die Äquivalenz der Ausdrucksstärke des deskriptiven und des algebraischen Ansatzes; Vorbemerkungen zum Thema Optimierung; Definition des Erfüllbarkeitsproblems, des Äquivalenzproblems und des Query Containment Problems; Einführung der Begriffe "Substitution", "Homomorphismus" (für Tableau-Anfragen) und "kanonische Datenbanken"; Formulierung und Beweis von Prop. 3.34 (in Vorbereitung auf den Homomorphismussatz)
Material:
Vorlesungsskript, Seiten 72-79
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: Wiederholung der Begriffe "Homomorphismus" und "kanonische Datenbank"; Formulierung und Beweis des Homomorphismussatzes; NP-Vollständigkeit des Query Containment Problems für Tableau-Anfragen
Material:
Vorlesungsskript, Seiten 79-83
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: Minimierung von Tableau-Anfragen; Greedy-Algorithmus zur Minimierung von Tableau-Anfragen (inkl. Korrektheitsbeweis); ein Beispiel zur Verwendung des Algorithmus zur Tableau-Minimierung
Material:
Vorlesungsskript, Seiten 83-89
Weitere Lektüre:
Kapitel 6.2 und 6.4 von [AHV]
Weiter mit Kapitel 3: Konjunktive Anfragen - heute: azyklische konjunktive Anfragen, Join-Bäume, Semijoin-Anfragen, ein effizienter Algorithmus zur Auswertung von Semijoin-Anfragen
Material:
Vorlesungsskript, Seiten 90-96
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 (insbes: Details zur Umwandlung einer gegebenen azyklischen Booleschen regelbasierten Anfrage Q und eines Join-Baums T von Q in eine zu Q äquivalente Boolesche Semijoin-Anfrage); ein Algorithmus zum Test auf Azyklizität und zum Erzeugen von Join-Bäumen: Beschreibung des Algorithmus und Betrachten von Beispiel-Läufen des Algorithmus für verschiedene Eingaben
Material:
Vorlesungsskript, Seiten 96-100
Weitere Lektüre:
Kapitel 6.2 und 6.4 von [AHV].
Weiter mit Kapitel 3: Konjunktive Anfragen - heute: Algorithmus zum Test auf Azyklizität und zum Erzeugen von Join-Bäumen: 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:
Vorlesungsskript, Seiten 100-103
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 argumentiert, 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 hinsichtlich der Multimengen-Semantik
Material:
Vorlesungsskript, Seiten 103-110
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.
Beginn mit Kapitel 5: Funktionale Abhängigkeiten - heute: Einführung ins Thema; Grundbegriffe zum Thema "funktionale Abhängigkeiten" und FD-Mengen; verlustfreie Joins (inkl. Beweis von Proposition 5.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
Material:
Vorlesungsskript, Seiten 161-168
Weitere Lektüre:
Kapitel 8.1, 8.2 und 8.4 von [AHV]
Weiter mit Kapitel 5: Funktionale Abhängigkeiten - heute: Nachweis, dass das Anwenden der FD-Regel die Äquivalenz bzgl. einer FD-Menge F erhält (Proposition 5.6); 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; ein Polynomialzeit-Algorithmus zum Entscheiden, ob eine FD f aus einer FD-Menge F folgt (Satz 5.17)
Material:
Vorlesungsskript, Seiten 168-174
Weitere Lektüre:
Kapitel 8.4 und 8.2 von [AHV]
Abschluss von Kapitel 5: Funktionale Abhängigkeiten - heute:
der Armstrong-Kalkül;
Nachweis der Vollständigkeit des Armstrong-Kalküls
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
Material:
Vorlesungsskript, Seiten 175-179 und 121-128 (bis einschl. Folie 147)
Weitere Lektüre:
Kapitel 8.2 von [AHV]
Weiter mit Kapitel 4: Datalog - heute: Wiederholung Syntax von Datalog;
der "immediate consequence-Operator" TP und der "Stufen-Operator" SP;
die Fixpunkt-Semantik von Datalog; Kleine Demo des Fixpunktprozesses
ein Algorithmus zum Auswerten von
Datalog-Anfragen (dessen Datenkomplexität in Polynomialzeit liegt);
Modellbasierte Semantik von Datalog und der Satz von Knaster und Tarski;
Beweisbasierte Semantik von Datalog, Fakten und Beweisbäume;
Monotonie von Datalog-Anfragen Q und deren Abschluss unter adom(Q)-Homomorphismen;
Material:
Vorlesungsskript, Seiten 121-130;
Demo: snippets of logic, Demonstration der Fixpunktberechnung
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: 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; 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:
Vorlesungsskript, Seiten 133-139;
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].
Weiter mit Kapitel 4: Datalog - heute: Satzes von Immerman und Vardi; 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 156-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
Abschluss von Kapitel 4: Datalog - heute:
Abschluss des Beweises der Unentscheidbarkeit des QCP für
Datalog-Anfragen;
Beweis der Unentscheidbarkeit des Äquivalenzproblems für Datalog-Anfragen;
Beschränktheit von Datalog-Programmen; nicht-rekursives Datalog (nr-Datalog), der Abhängigkeitsgraph eines
Datalog-Programms, Ausblick: Charakterisierung der Ausdrucksstärke von nr-Datalog
via SPCU-Algebra und positiv existentiellen Kalkül; Datalog mit Negation: semipositives Datalog mit Negation,
stratifiziertes Datalog mit Negation, nicht-rekursives Datalog mit Negation ;
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;
Wiederholung einiger aus der Veranstaltung DBS I bekannter Aspekte zur Anfrageauswertung und heuristischen Optimierung
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;
Satz (vorerst ohne Beweis), dass die relationale Algebra, der Relationenkalkül mit Active
Domain Semantik und der bereichsunabhängige Relationenkalkül dieselbe
Ausdrucksstärke haben
Material:
Folien 158-199 und 226-274,
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
Kapitel 5.1 und 6.1 von [AHV]
Beweises des Satzes, 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 zu zeigen,
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 258-281
Weitere Lektüre:
Kapitel 5.4 von [AHV]