|
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, Datenbankschemata und Datenbank(instanz)en, Beispieldatenbank mit Kinodaten
Material:
Folien 1-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:
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-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; Syntax und Semantik des konjunktiven Kalküls; eine Normalform für CQ; Beginn des Beweises der Äquivalenz der Ausdrucksstärke von Tableau-Anfragen, konjunktivem Kalkül und regelbasierten konjunktiven Anfragen
Material:
Folien 38-56,
Übungsblatt 1
Weitere Lektüre:
Teil A und Kapitel 4.1 und 4.2 von [AHV]
Weiter mit Kapitel 3: Konjunktive Anfragen - heute: Abschluss des Beweises der Äquivalenz der Ausdrucksstärke von Tableau-Anfragen, konjunktivem Kalkül und regelbasierten konjunktiven Anfragen; regelbasierte konjunktive Anfragen mit "="; regelbasierte konjunktive Programme; Auswertungskomplexität konjunktiver Anfragen: das Auswertungsproblem für CQ (kombinierte Komplexität) und die Größe von Anfragen und Datenbanken
Material:
Folien 56-66,
Übungsblatt 2
Weitere Lektüre:
Kapitel 4.3 von [AHV]
Weiter mit Kapitel 3: Konjunktive Anfragen - heute: 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:
Folien 66-70
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 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,
Übungsblatt 3
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 des Satzes von Chandra und Merlin; Folgerung aus der NP-Vollständigkeit; SPC-Algebra und SPJR-Algebra: Syntax,Semantik und viele Beispiele
Material:
Folien 77-93
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: viele Beispiele für Anfragen der SPJR-Algebra; 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
Material:
Folien 94-100,
Übungsblatt 4
Weitere Lektüre:
Kapitel 4.4, 4.5 und 6.2 von [AHV]
Weiter mit Kapitel 3: Konjunktive Anfragen - heute: 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 des Homomorphismussatzes
Material:
Folien 101-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,
Übungsblatt 5
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 109-116
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 (heute: Formulierung des Algorithmus und Beispielläufe des Algorithmus)
Material:
Folien 117-119
Weitere Lektüre:
Kapitel 6.2 und 6.4 von [AHV]
Abschluss von Kapitel 3: Konjunktive Anfragen - heute: ein Algorithmus zum Test auf Azyklizität und zum Erzeugen von Join-Bäumen (heute: Korrektheitsbeweis: Beweis von Behauptung 1. Ein Beweis von Behauptung 2 wird zu einem späteren Zeitpunkt nachgeliefert); 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 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
Material:
Folien 118-132
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.
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
Erster Zwischentest
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,
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.
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
Material:
Folien 155,
handschriftliche Notizen zum
Beweis von Satz 4.13 (Datalog zur Simulation von Turingmaschinen)
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: 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; 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,
Ü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:
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;
Idee zum Beweis der Unentscheidbarkeit der Beschränktheit von Datalog-Programmen
zur Information: Abschnitt 4.5 "Einschränkungen und Erweiterungen: nr-Datalog und Datalog mit Negation" wird in diesem Semester nicht behandelt
Material:
Folien 158-161,
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
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 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
Material:
Folien 182-191,
Übungsblatt 9
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 Ä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
Material:
Folien 191-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 und Beginn des Nachweises der Vollständigkeit des Armstrong-Kalküls
Material:
Folien 201-207;
Übungsblatt 10
Weitere Lektüre:
Kapitel 8.2 von [AHV]
Abschluss von Kapitel 5: Funktionale Abhängigkeiten - heute:
Abschluss des Nachweises der Vollständigkeit des Armstrong-Kalküls
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
Material:
Folien 206-235
Weitere Lektüre:
Kapitel 5.1 und 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; Beginn 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 241-254;
Übungsblatt 11
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 zu zeigen, dass es keinen Algorithmus gibt, der bei Eingabe einer Anfrage des Relationenkalküls entscheidet, ob die Anfrage bereichsunabhängig ist
Material:
Folien 254-257
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: den sicheren Relationenkalkül CALCsr eingeführt und an Beispielen illustriert; ein technisches Lemma zum Relationenkalkül CALCsr bewiesen
Material:
Folien 258-265
Weitere Lektüre:
Kapitel 5.4 von [AHV]
Abschluss von 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;
die Unentscheidbarkeit der statischen Analyse für relational vollständige
Anfragesprachen nachgewiesen;
Beweisidee zum Satz 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)
Kapitel 8: Zusammenfassung und Ausblick,
Abschluss der Veranstaltung,
Hinweise zur Vorbereitung auf eine mündliche Modulabschlussprüfung
Nachtrag zu Kapitel 3: Beweis von "Behauptung 2" innerhalb des Beweises von Lemma 3.45 (dies schließt den Korrektheitsbeweis des Algorithmus zum Test auf Azyklizität von regelbasierten konjunktiven Anfragen ab).
Material:
Folien 266-271 und 279-285 und 118-120
Weitere Lektüre:
Kapitel 5.4 und 6.3 von [AHV]