|
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. Start mit Kapitel 2: Aussagenlogik — heute:
Einführung und Beispiele.
Organisatorisches (entlang der Webseite der Vorlesung).
Material:
Folien 1-33,
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, Vereinbarungen und Notationen, Wahrheitstafeln, ein Logikrätsel, computerlesbare Darstellung von Formeln; Demo des Formelcheckers für die Aussagenlogik "snippets-of-logic"
Material:
Folien 34-63,
Skript Seiten 21-36,
Weitere Lektüre:
Kapitel 1 und 2.A in [KK],
Einleitung und Kapitel 1.1 in [S],
Kapitel 2.1 in [B].
Weiter mit Kapitel 2: Aussagenlogik — heute: Auflösung des Rätsels zur Geburtstagsfeier (Beispiel 2.1); Definition von Erfüllbarkeit, Allgemeingültigkeit, die Folgerungsbeziehung; Zusammenhänge zwischen Allgemeingültigkeit, Erfüllbarkeit und Folgerungsbeziehung; aussagenlogische Modellierung am Beispiel von Sudokus; aussagenlogische Modellierung am Beispiel der automatischen Hardwareverifikation
Material:
Folien 64-89,
Skript Seiten 36-49,
Weitere Lektüre:
Kapitel 1 und 2.A in [KK],
Einleitung und Kapitel 1.1 und 1.2 in [S],
Kapitel 2.4.1 und 2.5 in [B].
Weiter mit Kapitel 2: Aussagenlogik - heute: Äquivalenz von Formeln und Formelmengen; fundamentale Äquivalenzen; Beweise per Induktion über den Aufbau von Formeln; der Dualitätssatz der Aussagenlogik
Material:
Folien 90-101,
Skript Seiten 50-57,
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: Abschluss des Beweises des Dualitätssatzes; boolesche Funktionen und die funktionale Vollständigkeit der Aussagenlogik; Adäquatheit von Mengen von Junktoren und Konstanten
Material:
Folien 102-105,
Skript Seiten 57-60,
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: exklusives Oder, der Mehrheitsjunktor und der Sheffer-Strich (NAND-Gatter); Negationsnormalform (NNF) ein Beispiel zur Transformation in NNF; DNF und KNF; Beispiele und Algorithmen zur Transformation in DNF und KNF; eine kleine Formel mit großer DNF; der Endlichkeitssatz
Material:
Folien 106-125,
Skript Seiten 60-71
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: Beweises des Endlichkeitssatzes; 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
Material:
Folien 125-129,
Skript Seiten 71-77,
Weitere Lektüre:
Kapitel 2.B in [KK],
Kapitel 1.5 in [S],
Kapitel 2.10 in [B].
Weiter mit Kapitel 2: Aussagenlogik - heute: 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; Resolutionsableitungen und Resolutionswiderlegungen; Korrektheit und Vollständigkeit der Resolution (d.h.: eine Klauselmenge besitzt genau dann eine Resolutionswiderlegung, wenn sie unerfüllbar ist): Beweis der Korrektheit, Induktionsanfang für die Vollständigkeit, Illustration des Induktionsschritts an einem Beispiel
Material:
Folien 130-139,
Skript Seiten 78-85,
Weitere Lektüre:
Kapitel 2.B in [KK],
Kapitel 1.5 in [S],
Kapitel 2.10 in [B].
Weiter mit Kapitel 2: Aussagenlogik - heute: Abschluss des Beweises der Vollständigkeit der Resolution; Vorsicht beim Anwenden der Resolutionsregel; der Satz von Haken: Definition der pigeonhole-principle Klauselmenge, Demonstration des exponentiellen Anstiegs der Größe von computergenerierten Resolutionswiderlegungen (Bildschirmfoto); Algorithmen zur Lösung des (NP-vollständigen) aussagenlogischen Erfüllbarkeitsproblems: der Wahrheitstafelalgorithmus, der Resolutionsalgorithmus, der DPLL-Algorithmus (inkl. Beispiel)
Material:
Folien 141-150,
Skript Seiten 86-93,
Weitere Lektüre:
Kapitel 2.B in [KK],
Kapitel 1.5 in [S],
Kapitel 2.10 in [B].
Kapitel 2: Aussagenlogik - heute: Beweis der Vollständigkeit und Korrektheit des DPLL Algorithmus; Zusammenhang zwischen DPLL und Resolutionswiderlegungen (ohne Beweis); Demonstration von lingeling auf pigeonhole-pinciple Klauselmengen; Hornklauseln und Hornformeln; der Streichungsalgorithmus: ein effizienter Erfüllbarkeitsalgorithmus für Hornformeln (Algorithmus, Beispiel-Läufe, Laufzeitanalyse und Zusammenhang zu Resolution)
Material:
Folien 151-158,
Skript Seiten 93-99,
Weitere Lektüre:
Kapitel 3.A und 3.B in [KK],
Kapitel 1.3 in [S],
Kapitel 2.11 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.
Ein sehr guter Überblick über den Stand der Forschung zum Thema
"SAT-Solver" findet sich beispielsweise in der
Dissertation Towards Next Generation Sequential and Parallel
SAT Solvers von
Dr. Norbert
Manthey (TU Dresden, 2014).
Der in der Vorlesung Demonstrierte SAT-Solver lingeling kann unter http://fmv.jku.at/lingeling/ heruntergeladen werden. Als ein Generator für Klauselmengen (unter anderem für das pigeon-hole-principle) eignet sich CNFgen
Abschluss von Kapitel 2: Aussagenlogik - heute:
Korrektheitsbeweis des Streichungsalgorithmus; Zusammenfassung der Aussagenlogik: wichtige Begriffe, Sätze und Verfahren sowie Hinweise zur Klausurvorbereitung und mögliche Prüfungsfragen.
Start mit Kapitel 3: Logik erster Stufe - heute:
Signaturen und Strukturen
Material:
Folien 161-167,
Skript Seiten 101-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: Strukturen, Beispiele für Signaturen und Strukturen, Eigenschaftern 2-stelliger Relationen, Äquivalenzrelationen, Ordnungen, arithmetische Strukturen, Wörter als Strukturen, endliche Automaten als Strukturen (Transitionssysteme), relationale Datenbanken als Strukturen; Restriktionen und Expansionen; Isomorphie
Weiter mit Kapitel 3: Logik erster Stufe - heute: weitere Beispiele zur Isomorphie; Variablen und Terme der Logik erster Stufe, Belegungen, σ-Interpretationen, Semantik von Termen; Vergleich zwischen Aussagenlogik und Logik erster Stufe; Syntax der Logik erster Stufe; Beispiele zur Semantik der Logik erster Stufe; formale Definition der Semantik der Logik erster Stufe; viele Beispiele; die Modellbeziehung; Subterme, Subformeln und Syntaxbäume
Material:
Folien 189-219,
Skript Seiten 114-126,
Weitere Lektüre:
Kapitel III.1 und Kapitel II.1-3 in [EFT].
Weiter mit Kapitel 3: Logik erster Stufe - heute: Übung zur Sytax und Semantik der Logik erster Stufe; Formulierung des Isomorphielemmas der Logik erster Stufe (für Terme und Formeln); generelle Form von Beweisen per Induktion über den Aufbau von Termen und Formeln, Beweis des Isomorphielemmas
Material:
Folien 220-227,
Skript Seiten 127-132,
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: Abschluss des Beweises von Teil (b) des Isomorphielemmas (Induktionsschritt); das Koinzidenzlemma der Logik erster Stufe; freie Variablen; Sätze der Logik erster Stufe; Modellklassen und Definierbarkeit (bzw. Axiomatisierbarkeit) von Klassen von Strukturen; Beispiele für Formeln der Logik erster Stufe in verschiedenen Anwendungsbereichen: lineare Ordnungen, Arithmetik, Worte
Material:
Skript Seiten 131-142,
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: weitere Beispiele für Formeln der Logik erster Stufe in verschiedenen Anwendungsbereichen: Arithmetik, Datenbanken; eine andere Sicht auf die Semantik der Logik erster Stufe; 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; Beispiel eines Durchlaufes des Algorithmus
Material:
Skript Seiten 142-148
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 - (Abschnitt 3.7 zur Äquivalenz wird nächste Woche besprochen) heute: Abschnitt 3.8 Ehrenfeucht-Fraisse-Spiele: Spielregeln des m-Runden EF-Spiels, Gewinnbedingung, partielle Isomorphismen, Beispiele; Formalisierung des Begriffs "Gewinnstrategie"; der Begriff der Quantorentiefe einer FO-Formel; Formulierung und Beweis des Satzes von Ehrenfeucht (ohne Beweis); Beweis der einfachen Version des Satzes von Ehrenfeucht;
Material:
Skript Seiten 152-161,
Weitere Lektüre:
Kapitel 3.2 und 3.3 in [L],
Kapitel 4.3 in [FG]
Weiter mit Kapitel 3: Logik erster Stufe - heute: Abschluss des Beweises der einfachen Version des Satzes von Ehrenfeucht; Erklärung, wie Spoiler durch "Ausspielen einer Formel" eine Gewinnstrategie erhält; Begriff der FO-Definierbarkeit einer Klasse von σ-Strukturen, Korollar über nicht-FO-definierbare Klassen von σ-Strukturen; das EF-Spiel auf 2 endlichen linearen Ordnungen
Material:
Skript Seiten 161-166
Weitere Lektüre:
Kapitel 3.2 und 3.3 in [L]
Weiter mit Kapitel 3: Logik erster Stufe - heute: Weitere Anwendungen des Satzes von Ehrefeucht: die Klasse der regulären Graphen ist nicht FO-definierbar, die Klasse aller endlichen linearen Ordnungen gerader Kardinalität ist nicht FO-definierbar, die reguläre Sprache a(aa)* ist nicht FO-definierbar; Beweis des Resultats, das besagt, dass weder Graph-Zusammenhang noch Erreichbarkeit noch Kreisfreiheit FO-definierbar sind; Äquivalenz von Formeln der Logik erster Stufe
Material:
Folien 284-289, 259-264
Skript Seiten 166-170, Abschnitt 3.7 (Seiten 149-151)
Weitere Lektüre:
Kapitel 3.5 und 3.2 in [L]
Abschluss von Kapitel 3: Logik erster Stufe - heute:
weiter mit Äquivalenz von Formeln der Logik erster Stufe: gebundene Umbenennung, Quantorentausch, unnütze Quantoren, Beispiele äquivalenter Formeln;
Erfüllbarkeit, Allgemeingültigkeit und die
Folgerungsbeziehung für Formeln der Logik erster Stufe; die Formeln "Verum"
und "Falsum", weitere Beispiele; Normalformen für Formeln der Logik erster Stufe:
Negationsnormalform und Pränex-Normalform;
das Weihnachtstheorem
Material:
Folien 282-296,
Skript Abschnitt 3.7 (Seiten 149-151), Abschnitt 3.9 (Seiten 170-176)
Folien zum Weihnachtstheorem,
Weitere Lektüre:
Kapitel 3.2 und 3.6 in
[L],
Kapitel 2.2 in [S]
Wiederholung zum Folgerungsbegriff, Beweis der Korrektheit prädikatenlogischer Formulierungen zweier Syllogismen (von Aristoteles und Carroll); 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
Material:
Folien 305-318,
Skript Seiten 177-185
Weitere Lektüre:
Kapitel 3.6 in
[L],
Kapitel 2.2 in [S],
Weiter mit Kapitel 4: Grundlagen des automatischen Schließens - heute: 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 der Begriff der Korrektheit von Sequenzenregeln; Einführung und Korrektheit der Grundregeln (V) und (E) und der aussagenlogischen Regeln ( (FU), (W), etc ); Syntaktischer Beweis von modus ponens mit Hilfe aussagenlogischer Sequenzenregeln; Substitutionen und das Substitutionslemma (ohne Beweis); Einführung und Korrektheit der Quantorenregeln (∀A), (∀S), (∃A), (∃S); syntaktischer Beweis von Aristotles Syllogismus mit Hilfe von modus ponens und (∀A)
Material:
Folien 319-333,
Skript Seiten 185-195
Weitere Lektüre:
Kapitel IV.1-4, IV.6 und III.8 in [EFT],
Kapitel 2.2 in [S]
Weiter mit Kapitel 4: Grundlagen des automatischen Schließens - heute: Gleichheitsregeln; Ableitungen von Carrolls Syllogismus im Sequenzenkalkül kS; ein mittels Ableitungen im Sequenzenkalkül kS definierter Begriff der Beweisbarkeit von Formeln aus Formelmengen; Widerspruchsfreie und widerspruchsvolle Formelmengen; Eigenschaften widerspruchsvoller Formelmengen; der Vollständigkeitssatz und das Erfüllbarkeitslemma
Material:
Folien 334-343,
Skript Seiten 196-201,
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: Beweis des Vollständigkeitssatzes unter Verwendung des Erfüllbarkeitslemmas; Anmerkungen zum Beweis des Erfüllbarkeitslemmas; der Endlichkeitssatz (inkl. Beweis unter Verwendung des Vollständigkeitssatzes); erststufige Axiomatisierbarkeit; Anwendung des Endlichkeitssatzes zum Beweis der Nicht-Axiomatisierbarkeit der Endlichkeit
Material:
Folien 343-349,
Skript Seiten 202-207
Weitere Lektüre:
Kapitel IV.7, V und VI.1-3 in [EFT]
Weiter mit Kapitel 4: Grundlagen des automatischen Schließens - heute: Kochrezept für das Beweisen von Nicht-Axiomatisierbarkeitsresultaten mit dem Endlichkeitssatz und die Nicht-Axiomatisierbarkeit von Graphzusammenhang; der Satz von Löwenheim und Skolem (ohne Beweis) inkl. Anwendung des Satzes; Einführung ins Thema "die Grenzen der Berechenbarkeit": Entscheidungsprobleme, Entscheidbarkeit, Semi-Entscheidbarkeit; 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
Material:
Folien 350-358,
Skript Seiten 208-216,
Weitere Lektüre:
Kapitel VI.1-3 und X.1-4 in [EFT]
Kapitel 2.3 in [S]
Weiter mit Kapitel 4: Grundlagen des automatischen Schließens - heute: Nachweis der Unentscheidbarkeit des Allgemeingültigkeitsproblems für die Logik erster Stufe (durch Nutzen der Unentscheidbarkeit des Postschen Korrespondenzproblems); Start von Abschnitt 4.5 über den Satz von Herbrand: Grundterme, Herbrandstrukturen
Material:
Folien 359-367,
Skript 216-223,
Weitere Lektüre:
Kapitel 2.4 in [S] und
Kapitel XI.1-3 in [EFT]
Weiter mit Abschnitt 4.5 über den Satz von Herbrand: Herbrandmodelle, gleichheitsfreie Formeln in Skolemform, 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 von Herbrand
Material:
Folien 368-373,
Skript 223-229,
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: Skolemisierung, Grundlagen von automatischen Theorembeweisern, inkl. Beispiel
Material:
Folien 374-379,
Skript Seiten
229-234,
Weitere Lektüre:
Kapitel 2.4 in [S]
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
Material:
Folien 379-404,
Skript 235-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; Zusammenhang zwischen Logikprogrammen, Logik erster Stufe, Herbrandexpansion und Hornformeln; Diskussion zur Unentscheidbarkeit von Logikprogrammen anhand eines Logikprogramms für das Postsche Korrespondenzproblem ( pcp.pl) operationelle Semantik; ANTWORT(Π,α) (ein einfacher Interpreter für Logikprogramme); Korrektheit und Vollständigkeit des Interpreters (ohne Beweis); Unifikatoren; Beispiele zur Unifikation; Äquivalenz und Allgemeinheit von Substitutionen; allgemeinste Unifikatoren (engl.: mgu - für most general unifiers)
Material:
Folien 405-425,
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: Eindeutigkeit von allgemeinsten Unifikatoren; der Unifikationsalgorithmus; Beispiele zur Anwendung des Algorithmus 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 425-Ende
Skript 263-Ende
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.
