|
Logik in der Informatik
Prof. Dr. Nicole Schweikardt |
|
Hier finden Sie (nach den Vorlesungen) Informationen zum Inhalt der einzelnen Vorlesungsstunden, die in der Vorlesung verwendeten Folien, Teile des Skripts und gelegentlich auch Korrekturen und sonstige ergänzende Bemerkungen.
Kapitel 1: Einführung ins Thema "Logik in der
Informatik" — Paradoxien, Syllogismen, Anwendungen der Logik in der
Informatik, Logik-Programmierung und Prolog
Organisatorisches (entlang der Webseite der Vorlesung).
Start mit Kapitel 2: Aussagenlogik — heute: Einführung und Beispiel
Material:
Folien 1-30,
Skript Seiten 1-21
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.
Weiter mit Kapitel 2: Aussagenlogik - heute: Syntax und Semantik der Aussagenlogik, rekursive Definitionen über Formeln, Modelle, das Koinzidenzlemma, Wahrheitstafeln, ein Logikrätsel, computerlesbare Darstellung von Formeln
Material:
Folien 30-60,
Skript Seiten 21-35,
Formelchecker für die Aussagenlogik: snippets-of-logic
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: Demo des Formelcheckers für die Aussagenlogik "snippets-of-logic"; Auflösung des Rätsels zur Geburtstagsfeier (Beispiel 2.1); Erfüllbarkeit, Allgemeingültigkeit, die Folgerungsbeziehung; Modus Ponens; Zusammenhänge zwischen Allgemeingültigkeit, Erfüllbarkeit und Folgerungsbeziehung; aussagenlogische Modellierung am Beispiel von Sudokus
Material:
Folien 60-79,
Skript Seiten 35-46,
Formelchecker für die Aussagenlogik: snippets-of-logic,
Übungsblatt 1
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 der automatischen Hardwareverifikation; Äquivalenz von Formeln und Formelmengen; fundamentale Äquivalenzen; Beweise per Induktion über den Aufbau von Formeln der Dualitätssatz
Material:
Folien 80-96,
Skript Seiten 46-57
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: boolesche Funktionen und die funktionale Vollständigkeit der Aussagenlogik; Adäquatheit von Mengen von Junktoren und Konstanten; exklusives Oder, der Mehrheitsjunktor und der Sheffer-Strich (NAND-Gatter); Negationsnormalform (NNF) ein Beispiel zur Transformation in NNF; DNF und KNF
Material:
Folien 97-114,
Skript Seiten 57-67,
Übungsblatt 2
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: Beispiele und Algorithmen zur Transformation in NNF, DNF und KNF; eine kleine Formel mit großer DNF; der Endlichkeitssatz
Material:
Folien 115-120,
Skript Seiten 68-73
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: Beispiel für eine Anwendung des Endlichkeitssatzes (um nachzuweisen, 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; das Resolutionslemma
Material:
Folien 121-129,
Skript Seiten 73-81,
Übungsblatt 3
Weitere Lektüre:
Kapitel 2.B in [KK],
Kapitel 1.5 in [S],
Kapitel 2.10 in [B].
Weiter mit Kapitel 2: Aussagenlogik - heute: Resolutionsableitungen und Resolutionswiderlegungen; 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
Material:
Folien 130-135,
Skript Seiten 81-86,
Weitere Lektüre:
Kapitel 2.B in [KK],
Kapitel 1.5 in [S],
Kapitel 2.10 in [B].
Weiter mit Kapitel 2: Aussagenlogik - heute: der Satz von Haken (ohne Beweis); Algorithmen zur Lösung des (NP-vollständigen) aussagenlogischen Erfüllbarkeitsproblems: der Wahrheitstafelalgorithmus, der Resolutionsalgorithmus, der DPLL-Algorithmus (inkl. Beispiel)
Material:
Folien 136-145,
Skript Seiten 86-93,
Übungsblatt 4
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.
Abschluss von Kapitel 2: Aussagenlogik - heute:
Hornklauseln und Hornformeln; der Streichungsalgorithmus: ein
effizienter Erfüllbarkeitsalgorithmus für Hornformeln (Algorithmus,
Beispiel-Läufe, Laufzeitanalyse und Korrektheitsbeweis)
Start mit Kapitel 3: Logik erster Stufe - heute:
Signaturen und Strukturen
Material:
Folien 146-158,
Skript Seiten 93-103
Weitere Lektüre:
Kapitel 3.A und 3.B in [KK],
Kapitel 1.3 in [S],
Kapitel 2.11 in [B].
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: Signaturen und Strukturen, Eigenschaftern 2-stelliger Relationen, Äquivalenzrelationen, Ordnungen, arithmetische Strukturen, Wörter als Strukturen, Transitionssysteme, relationale Datenbanken als Strukturen; Restriktionen und Expansionen
Material:
Folien 155-174,
Skript Seiten 101-110
Übungsblatt 5
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: Isomorphie, Variablen, Terme der Logik erster Stufe, Belegungen, Interpretationen, Semantik von Termen, Vergleich zwischen Aussagenlogik und Logik erster Stufe, Syntax der Logik erster Stufe
Material:
Folien 175-197,
Skript Seiten
111-120
Weitere Lektüre:
Kapitel III.1 und Kapitel II.1-3 in [EFT].
Weiter mit Kapitel 3: Logik erster Stufe - heute: Semantik der Logik erster Stufe; viele Beispiele; die Modellbeziehung; Subterme, Subformeln und Syntaxbäume; Formulierung des Isomorphielemmas der Logik erster Stufe (für Terme und Formeln); generelle Form von Beweisen per Induktion über den Aufbau von Termen und Beweis von Teil (a) des Isomorphielemmas (Aussage für Terme)
Material:
Folien 198-217,
Skript Seiten 121-129,
Übungsblatt 6
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: generelle Form von Beweisen per Induktion über den Aufbau von Formeln der Logik erster Stufe; Beweis von Teil (b) des Isomorphielemmas (Aussage für Formeln); das Koinzidenzlemma der Logik erster Stufe; freie Variablen; Sätze der Logik erster Stufe; Modellklassen und Definierbarkeit (bzw. Axiomatisierbarkeit) von Klassen von Strukturen
Material:
Folien 215-228,
Skript Seiten 130-137
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]
Weiter mit Kapitel 3: Logik erster Stufe - heute: Beispiele für Formeln der Logik erster Stufe in verschiedenen Anwendungsbereichen: lineare Ordnungen, Arithmetik, Worte, Datenbanken; eine andere Sicht auf die Semantik der Logik erster Stufe
Material:
Folien 229-246,
Skript Seiten 138-146,
Übungsblatt 7
Weitere Lektüre:
Kapitel II.5 und Kapitel III.4 und III.6
in [EFT],
Kapitel 1.1 in [L]
Weiter mit Kapitel 3: Logik erster Stufe - heute: 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; relationale Signaturen; Ehrenfeucht-Fraisse-Spiele: Spielregeln des m-Runden EF-Spiels, Gewinnbedingung, partielle Isomorphismen, ein Beispiel
Material:
Folien 245-260,
Skript Seiten 145-153
Weitere Lektüre:
Kapitel 3.2 und 3.3 in [L],
Kapitel 4.3 in [FG]
Weiter mit Kapitel 3: Logik erster Stufe - heute: Ehrenfeucht-Fraisse-Spiele: Beispiele; Formalisierung des Begriffs "Gewinnstrategie"; Formulierung des Satzes von Ehrenfeucht (ohne Beweis); der Begriff der Quantorentiefe einer FO-Formel; Erklärung, wie Spoiler durch "Ausspielen einer Formel" eine Gewinnstrategie erhält; Formulierung und Beginn des Beweises der einfachen Version des Satzes von Ehrenfeucht
Material:
Folien 259-270,
Skript Seiten
152-159 und 162,
Übungsblatt 8
Weitere Lektüre:
Kapitel 3.2 und 3.3 in [L]
Weiter mit Kapitel 3: Logik erster Stufe - heute: Abschluss des Beweises der einfachen Version des Satzes von Ehrenfeucht; Begriff der FO-Definierbarkeit einer Klasse von σ-Strukturen, Korollar über nicht-FO-definierbare Klassen von σ-Strukturen; das EF-Spiel auf 2 endlichen linearen Ordnungen; Nachweis, dass Duplicator eine Gewinnstrategie im m-Runden EF-Spiel auf 2 endlichen linearen Ordnungen der Kardinalität > 2^m besitzt (Beginn des Beweises)
Material:
Folien 270-275,
Skript Seiten
159-166
Weitere Lektüre:
Kapitel 3.5 und 3.2 in [L]
Weiter mit Kapitel 3: Logik erster Stufe - heute: Abschluss des Beweises, dass Duplicator eine Gewinnstrategie im m-Runden EF-Spiel auf 2 endlichen linearen Ordnungen der Kardinalität > 2^m besitzt; Folgerung, dass die Klasse aller endlichen linearen Ordnungen gerader Kardinalität nicht FO-definierbar ist; Beweis des Resultats, das besagt, dass weder Graph-Zusammenhang noch Erreichbarkeit FO-definierbar sind; Bemerkung zur Methode der logischen Reduktionen
Material:
Folien 274-281,
Skript Seiten 164-170,
Übungsblatt 9
Weitere Lektüre:
Kapitel 3.2 und 3.6 in
[L]
Abschluss von Kapitel 3: Logik erster Stufe - heute: Erfüllbarkeit, Allgemeingültigkeit und die Folgerungsbeziehung für Formeln der Logik erster Stufe; die Formeln "Verum" und "Falsum"; Normalformen für Formeln der Logik erster Stufe: Negationsnormalform und Pränex-Normalform
Material:
Folien 282-293,
Skript Seiten 170-176
Weitere Lektüre:
Kapitel 3.6 in
[L],
Kapitel 2.2 in [S],
Start mit Kapitel 4: Grundlagen des automatischen Schließens - heute: Ableitungsregeln, Kalküle, Ableitungen, Beispiele für Kalküle (zur Definition bestimmter Mengen natürlicher Zahlen, zur Definition der syntaktisch korrekten aussagenlogischen Formeln, Resolutionskalkül der Aussagenlogik); Mengen, die unter einem Kalkül abgeschlossen sind; Charakterisierung aller aus einer Menge V in einem Kalkül K ableitbaren Elemente als die kleinste unter K abgeschlossene Menge, die jedes Element aus V enthält; Induktionsprinzip für die Menge der ableitbaren Elemente eines Kalküls; Notationen für Logik erster Stufe, der Begriff einer "Sequenz", die Menge MS aller Sequenzen, Korrektheit von Sequenzen; Korrektheit, Vollständigkeit und Effektivität von Kalkülen über der Menge MS
Material:
Folien 294-311,
Skript 177-188,
Übungsblatt 10
Weitere Lektüre:
Kapitel IV.1 in [EFT],
Weiter mit Kapitel 4: Grundlagen des automatischen Schließens - heute: der Begriff der Korrektheit von Sequenzenregeln; Einführung und Korrektheit der Grundregeln (V) und (E) und der aussagenlogischen Regeln ( (FU), (W), etc ); Substitutionen und das Substitutionslemma (ohne Beweis).
Material:
Folien 312-320,
Skript 188-193
Weitere Lektüre:
Kapitel IV.2-3, IV.6 und III.8 in [EFT],
Kapitel 2.2 in [S]
Weiter mit Kapitel 4: Grundlagen des automatischen Schließens - heute: Einführung und Korrektheit der Quantorenregeln (Einführung des Allquantors im Antezdens, Einführung des Allquantors im Sukzedens, Einführung des Existenzquantors im Antezedens, Einführung des Existenzquantors im Sukzedens) und der Gleichheitsregeln (G) und (S); Einführung und Korrektheit des Sequenzenkalküls kS; Anmerkungen zur Effektivität des Sequenzenkalküls kS; Beispiele für Ableitungen im Sequenzenkalkül kS
Material:
Folien 320-327,
Skript
Seiten 193-198,
Übungsblatt 11
Weitere Lektüre:
Kapitel IV.2-4, IV.6 und III.8 in [EFT],
Kapitel 2.2 in [S]
Weiter mit Kapitel 4: Grundlagen des automatischen Schließens - heute: noch ein Beispiel für eine Ableitung im Sequenzenkalkül kS; ein mittels Ableitungen im Sequenzenkalkül kS definierter Begriff der Beweisbarkeit von Formeln aus Formelmengen; Widerspruchsfreie und widerspruchsvolle Formelmengen; der Vollständigkeitssatz und das Erfüllbarkeitslemma; Beweis des Vollständigkeitssatzes unter Verwendung des Erfüllbarkeitslemmas Formulierung des Endlichkeitssatzes
Material:
Folien 327-334,
Skript Seiten 199-203
Weitere Lektüre:
Kapitel IV.7, V und VI.2 in [EFT]
Weiter mit Kapitel 4: Grundlagen des automatischen Schließens - heute: Beweis des Endlichkeitssatzes der Logik erster Stufe (unter Verwendung des Vollständigkeitssatzes); erststufige Axiomatisierbarkeit; Beweis der Nicht-Axiomatisierbarkeit der Endlichkeit und der Nicht-Axiomatisierbarkeit von Graph-Zusammenhang; der Satz von Löwenheim und Skolem (ohne Beweis) inkl. Anwendung des Satzes
Material:
Folien 334-340,
Skript Seiten
203-210,
Übungsblatt 12
Weitere Lektüre:
Kapitel VI.1-3 in [EFT]
Weiter mit Kapitel 4: Gundlagen des automatischen Schließens - heute: die Grenzen der Berechenbarkeit: Entscheidungsprobleme für die Logik erster Stufe, die Semi-Entscheidbarkeit des Allgemeingültigkeitsproblems, des Unerfüllbarkeitsproblems und des Folgerungsproblems für die Logik erster Stufe, Nachweis der Unentscheidbarkeit dieser Probleme (durch Nutzen der Unentscheidbarkeit des Postschen Korrespondenzproblems), Nachweis der Nicht-Semi-Entscheidbarkeit des Erfüllbarkeitsproblems für die Logik erster Stufe
Material:
Folien 341-354,
Skript Seiten
210-220
Weitere Lektüre:
Kapitel 2.3 in [S] und
Kapitel X.1-4 in [EFT]
Weiter mit Kapitel 4: Grundlagen des automatischen Schließens - heute: Abschluss des Beweises der Unentscheidbarkeit des Allgemeingültigkeitsproblems der Logik erster Stufe; Beginn des Abschnitts über den Satz von Herbrand: Grundterme, Herbrandstrukturen, Herbrandmodelle, gleichheitsfreie Formeln in Skolemform, die Herbrand-Expansion eines gleichheitsfreien Satzes in Skolemform
Material:
Folien 349-361,
Skript Seiten
217-225;
Übungsblatt 13 wird erst am Donnerstag (28.01.2016) ausgeteilt.
Weitere Lektüre:
Kapitel 2.4 in [S] und
Kapitel XI.1 in [EFT]
Weiter mit Kapitel 4: Grundlagen des automatischen Schließens - heute: die aussagenlogische Version der Herbrand-Expansion eines gleichheitsfreien Satzes in Skolemform, der Satz von Gödel-Herbrand-Skolem, der Satz von Herbrand, Anwendung des Satzes, Skolemisierung, Grundlagen von automatischen Theorembeweisern
Material:
Folien 361-365,
Skript Seiten
225-232,
Übungsblatt 13
Weitere Lektüre:
Kapitel 2.4 in [S] und
Kapitel XI.1-3 in [EFT]
Abschluss von Kapitel 4: Grundlagen des automatischen Schließens
- heute: Grundlagen von automatischen Theorembeweisern, inkl. Beispiel
Start mit Kapitel 5: Logik-Programmierung - heute:
Einführung ins Thema ("deklarativ" vs. "imperativ") und Anwendungsgebiete der
Logikprogrammierung;
Syntax und Semantik von Logikprogrammen: Fakten, Anfragen,
Variablen, Regeln,
Atome, Zahlen, Konstanten, Terme,
Substitutionen, Anwendung von Substitutionen, Instanzen von Termen,
Grundterme und Grundinstanzen, Ableitungen aus Logikprogrammen,
Beweisbäume, deklarative Semantik von Logikprogrammen: formale
Definition der
Bedeutung eines Programms und der Antwort auf eine Anfrage; viele Beispiele
Material:
Folien 366-396,
Skript 232-249
Weitere Lektüre:
Kapitel 3.1-3.3 in [S],
Introduction und Chapter 1 (Basic Constructs) in [SS],
Kapitel 3.C in [KK],
Kapitel XI.7 in [EFT]
Weiter mit Kapitel 5: Logik-Programmierung - heute: ein Beispiel zum Unterschied zwischen Theorie und Praxis (Wege in gerichteten Graphen); Anfragen an Logikprogramme; operationelle Semantik; ANTWORT(Π,α) (ein einfacher Interpreter für Logikprogramme); Korrektheit und Vollständigkeit des Interpreters (ohne Beweis); Unifikatoren; Beispiele zur Unifikation
Material:
Folien 397-415,
Skript 249-263
Weitere Lektüre:
Introduction und Teil I (also Chapter 1, 2, 3, 4 und 5) in [SS],
Kapitel 3.1-3.3 in [S],
Kapitel XI.7 in [EFT]
Abschluss von Kapitel 5: Logik-Programmierung - heute: Äquivalenz und Allgemeinheit von Substitutionen; allgemeinste Unifikatoren (engl.: mgu - für most general unifiers), der Unifikationsalgorithmus MGU(t,s); UANTWORT(Π,α) (ein Interpreter für Logikprogramme mit allgemeinsten Unifikatoren); Korrektheit und Vollständigkeit des Interpreters (ohne Beweis); Reines Prolog; ein Prolog-Interpreter PErsteANTWORT(Π,α); linksrekursive Regeln; Beispiele zum Unterschied zwischen Theorie und Praxis (d.h. Logik-Programmierung und Prolog)
Material:
Folien 415-433,
Skript 262-274
Weitere Lektüre:
Introduction und Teil I (also Chapter 1, 2, 3, 4 und 5) in [SS],
Kapitel 3.1-3.3 in [S],
Kapitel XI.7 in [EFT]
Hilfestellungen zur Klausurvorbereitung. Inbes.: Details zum Ablauf der Klausur und Durcharbeiten einiger Beispiel-Aufgaben
Material: Eine Zusammenstellung wichtiger Informationen sowie die in der Vorlesungsstunde verwendeten Beispielaufgaben finden Sie hier.