|
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 bis zum Ende von Abschnitt 2.1
Material:
Folien 1-22
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: 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 23-37
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 38-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 Semntik des konjunktiven Kalküls; eine Normalform für CQ; Äquivalenz der Ausdrucksstärke von Tableau-Anfragen, konjunktivem Kalkül und regelbasierten konjunktiven Anfragen
Material:
Folien 46-58
Weitere Lektüre:
Teil A und Kapitel 4.1 und 4.2 von [AHV]
Weiter mit Kapitel 3: Konjunktive Anfragen - heute: Bereichsbeschränkte konjunktive Anfragen mit "="; 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 59-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: Abschluss des Beweises der NP-Vollständigkeit des Auswertungsproblems (kombinierte Komplexität) für Boolesche regelbasierte konjunktive Anfragen (ein Satz von Chandra und Merlin); SPC-Algebra und SPJR-Algebra: Syntax, Semantik und viele Beispiele
Material:
Folien 77-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; Einführung der Begriffe "Substitution" und "Homomorphismus" (für Tableau-Anfragen)
Material:
Folien 95-104
Weitere Lektüre:
Kapitel 4.4, 4.5 und 6.2 von [AHV]
Weiter mit Kapitel 3: Konjunktive Anfragen - heute: Kanonische Datenbanken eingeführt, den Homomorphismussatz bewiesen und die NP-Vollständigkeit des Query Containment Problems für Tableau-Anfragen nachgewiesen.
Material:
Folien 104-107,
Übungsblatt 4
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
Material:
Folien 108-110
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: azyklische konjunktive Anfragen, Join-Bäume, Semijoin-Anfragen, ein effizienter Algorithmus zur Auswertung von Semijoin-Anfragen
Material:
Folien 111-117,
Übungsblatt 5
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; ein Algorithmus zum Test auf Azyklizität und zum Erzeugen von Join-Bäumen
Material:
Folien 117-120
Weitere Lektüre:
Kapitel 6.2 und 6.4 von [AHV]
Weiter mit Kapitel 3: Konjunktive Anfragen - heute: Nachweis der Korrektheit des Algorithmus zum Test auf Azyklizität und zum Erzeugen von Join-Bäumen; 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; 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. Beginn eines kurzen Überblicks über die Multimengen-Semantik konjunktiver Anfragen
Material:
Folien 118-127,
Übungsblatt 6
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:
die Multimengen-Semantik regelbasierter konjunktiver Anfragen; Überblick
über Forschungsergebnisse und offene Forschungsfragen; Zusammenfassung der
wichtigsten in Kapitel 3 behandelten Themen
Start mit Kapitel 4: Datalog - heute:
einführendes Beispiel; Syntax von Datalog; der "immediate consequence operator"
Material:
Folien 127-140
Weitere Lektüre:
Kapitel 6.2 und 6.4 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 4: Datalog - heute: Fixpunkt-Semantik von Datalog; ein Algorithmus zum Auswerten von Datalog-Anfragen (dessen Datenkomplexität in Polynomialzeit liegt); logspace-Reduktionen und PTIME-Vollständigkeit eines Problems; Beginn des Beweises eines Satzes von Immerman und Vardi, der besagt, dass das Auswertungsproblem für Datalog-Anfragen bzgl. Datenkomplexität PTIME-vollständig ist
Material:
Folien 141-145
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: Abschluss des Beweises eines Satzes von Immerman und Vardi, der besagt, dass das Auswertungsproblem für Datalog-Anfragen bzgl. Datenkomplexität PTIME-vollständig ist (insbes.: Konstruktion eines Datalog-Programms PM, das bei Eingabe einer Datenbank Iw, die ein Wort w repräsentiert, den Lauf der Turingmaschine M bei Eingabe w simuliert)
Material:
Folien 141-145,
handschriftliche
Notizen zur PTIME-Vollständigkeit des AWP für Datalog (bzgl. Datenkomplexität)
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: Modellbasierte Semantik von Datalog und der Satz von Knaster und Tarski; Beweisbasierte Semantik von Datalog, Fakten und Beweisbäume; 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 146-153,
Ü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
Weiter mit Kapitel 4: Datalog - heute: Beweis der Unentscheidbarkeit des QCP für Datalog-Anfragen; Beschränktheit von Datalog-Programmen; Beweis der Unentscheidbarkeit der Beschränktheit von Datalog-Programmen
Material:
Folien 153-156
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 157-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
Abschluss von Kapitel 4: Datalog - heute: Datalog mit Negation: semipositives Datalog mit Negation, stratifiziertes Datalog mit Negation, nicht-rekursives Datalog mit Negation
Material:
Folien 162-175
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
Start mit Kapitel 5: 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; Anfrageauswertung und heuristische Optimierung
Material:
Folien 176-198,
Übungsblatt 9
Weitere Lektüre:
Kapitel 5.1 und 6.1 von [AHV]
Abschluss von Kapitel 5: Relationale Algebra - heute:
heuristische Optimierung; Join-Reihenfolge, SIP-Graph und SIP-Strategien
Start mit Kapitel 6: 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
Material:
Folien 198-222,
Übungsblatt 10
Weitere Lektüre:
Kapitel 5.3 von [AHV]
Weiter mit Kapitel 6: Relationenkalkül - heute: bewiesen, 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 beweisen, dass es keinen Algorithmus gibt, der bei Eingabe einer Anfrage des Relationenkalküls entscheidet, ob die Anfrage bereichsunabhängig ist
Material:
Folien 222-225
Weitere Lektüre:
Kapitel 5.3 von [AHV];
zum Satz von Trakhtenbrot siehe Kapitel 9.1 von [L]
Weiter mit Kapitel 6: Relationenkalkül - heute: Den sicheren Relationenkalkül CALCsr eingeführt, an Beispielen illustriert und bewiesen, dass der sichere Relationenkalkül bereichsunabhängig ist
Material:
Folien 226-233,
Übungsblatt 11
Weitere Lektüre:
Kapitel 5.4 von [AHV]
Weiter mit Kapitel 6: Relationenkalkül - heute: nachgewiesen, dass der sichere Relationenkalkül CALCsr bereichsunabhängig ist und genau dieselbe Ausdrucksstärke wie die relationale Algebra hat; 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)
Material:
Folien 233-239
Weitere Lektüre:
Kapitel 5.4 und 6.3 von [AHV]
Weiter mit Kapitel 6: Relationenkalkül - heute: Wiederholung: Beweis von Satz 6.19 (Unentscheidbarkeit der statischen Analyse Probleme für die Relationale Algebra); 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; den Begriff der Gaifman-Lokalität von Anfragen eingeführt und den Satz zitiert (ohne Beweis), der besagt, dass jede Anfrage des Relationenkalküls Gaifman-lokal ist; diesen Satz benutzt, um zu zeigen, dass die Anfrage "Gib alle Knoten des gerichteten Graphen aus, die von einem roten Knoten aus erreichbar sind" nicht im Relationenkalkül ausgedrückt werden kann.
Material:
Folien 236 und
240-245,
Übungsblatt 12
Weitere Lektüre:
Kapitel 5.4 und 6.3 von [AHV]
Abschluss von Kapitel 6: Relationenkalkül - heute:
die Gaifman-Lokalität des Relationenkalküls benutzt um zu zeigen, dass die
Anfrage "Gib alle Stationen aus, die von Bockenheimer Warte aus ohne
Umsteigen zu erreichen sind" nicht im Relationenkalkül formuliert
werden kann.
Beginn mit Kapitel 7: Funktionale Abhängigkeiten - heute:
Grundbegriffe zum Thema "funktionale Abhängigkeiten" und FD-Mengen; verlustfreie Joins
(inkl. Beweis von Proposition 7.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:
Folien 246-256
Weitere Lektüre:
Kapitel 8.1 und 8.2 von [AHV]
Weiter mit Kapitel 7: Funktionale Abhängigkeiten - heute: die FD-Regel, Verfolgungssequenzen und deren Eigenschaften, ein Polynomialzeit-Algorithmus zur Berechnung von chase(T,t,F)
Material:
Folien 256-263,
Übungsblatt 13
Weitere Lektüre:
Kapitel 8.4 von [AHV]
Weiter mit Kapitel 7: Funktionale Abhängigkeiten - heute: Algorithmen für Query Containment und Äquivalenz von konjunktiven Anfragen relativ zu einer FD-Menge, Minimierung von konjunktiven Anfragen relativ zu einer FD-Menge; ein Polynomialzeit-Algorithmus zum Entscheiden, ob eine FD f aus einer FD-Menge F folgt; der Armstrong-Kalkül
Material:
Folien 263-271
Weitere Lektüre:
Kapitel 8.4 und 8.2 von [AHV]
Abschluss von Kapitel 7: Funktionale Abhängigkeiten - heute:
Nachweis der Vollständigkeit des Armstrong-Kalküls
Kapitel 8: Zusammenfassung und Ausblick
Material:
Folien 271-278
Weitere Lektüre:
Kapitel 8.2 von [AHV]
Abschluss der Veranstaltung, Hinweise zur Vorbereitung auf eine mündliche Modulabschlussprüfung