|
Logik in der Informatik
Prof. Dr. Nicole Schweikardt |
|
In diesem Logbuch finden Sie (nach den Vorlesungen) Informationen zum Inhalt der einzelnen Vorlesungsstunden, die entsprechenden Teile des Skripts und gelegentlich auch Korrekturen und sonstige ergänzende Bemerkungen.
Am Dienstag, den 18.10.22 fand die Eröffnungsvorlesung statt.
Kapitel 1: Einführung ins Thema "Logik in der Informatik" — heute:
Paradoxien, Syllogismen, Anwendungen der Logik in der
Informatik, Logik-Programmierung und Prolog.
Organisatorisches (entlang der Webseite der Vorlesung).
Material:
Skript Seiten 1-15
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.
Ende von Kapitel 1: Einführung ins Thema "Logik in der Informatik" — heute:
Hintergrundinformationen zur Logik-Programmierung und zur Programmiersprache Prolog
Start mit Kapitel 2: Aussagenlogik — heute:
Einführung und Beispiele, Syntax und Semantik der
Aussagenlogik
Material:
Skript Seiten 15-30
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: 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"; Auflösung des Rätsels zur Geburtstagsfeier (Beispiel 2.1); Erfüllbarkeit, Allgemeingültigkeit
Material:
Skript Seiten 30-42,
Formelchecker für die Aussagenlogik: snippets-of-logic
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: die Folgerungsbeziehung; Modus Ponens; Zusammenhänge zwischen Allgemeingültigkeit, Erfüllbarkeit und Folgerungsbeziehung; aussagenlogische Modellierung am Beispiel von Sudokus; kurze Info zur aussagenlogischen Modellierung am Beispiel der automatischen Hardwareverifikation (Details hierzu finden sich im Vorlesungsskript)
Material:
Skript Seiten 42-51
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: Äquivalenz von Formeln und Formelmengen; fundamentale Äquivalenzen; Beweise per Induktion über den Aufbau von Formeln; der Dualitätssatz der Aussagenlogik (inkl. Beweis)
Material:
Skript Seiten 52-58
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; detaillierter Beweis der Adäquatheit von {¬,∨}; detaillierter Beweis der Nicht-Adäquatheit von {∅} und {∨, ∧, →}; exklusives Oder, der Mehrheitsjunktor und der Sheffer-Strich (NAND-Gatter)
Material:
Skript Seiten 58-64
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: Beweis der Adäquatheit von {|} (wobei | den Sheffer-Strich (also das NAND-Gatter) bezeichnet; Negationsnormalform (NNF), Disjunktive Normalform (DNF) und Konjunktive Normalform (KNF); Beispiele und Algorithmen zur Transformation in NNF, DNF und KNF
Material:
Skript Seiten 64-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: der Endlichkeitssatz der Aussagenlogik
Material:
Skript Seiten 73-78
Weitere Lektüre:
Kapitel 2.B in [KK],
Kapitel 1.5 in [S],
Kapitel 2.10 in [B].
Weiter mit Kapitel 2: Aussagenlogik - heute: Bemerkungen zum 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
Material:
Skript Seiten 78-82
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 Begriff einer Resolvente zweier Klauseln; das Resolutionslemma (inkl. Beweis); Resolutionsableitungen und Resolutionswiderlegungen; Korrektheit und Vollständigkeit der Resolution (d.h.: eine Klauselmenge besitzt genau dann eine Resolutionswiderlegung, wenn sie unerfüllbar ist)
Material:
Skript Seiten 83-88
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 (ohne Beweis); Algorithmen zur Lösung des (NP-vollständigen) aussagenlogischen Erfüllbarkeitsproblems: der Wahrheitstafelalgorithmus, der Resolutionsalgorithmus, der DPLL-Algorithmus (inkl. Beispiel)
Material:
Skript Seiten 87-96
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.
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).
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, Strukturen, Beispiele für Signaturen und Strukturen
Material:
Skript Seiten 96-107
Weitere Lektüre:
Kapitel 1.3 in [S],
Kapitel 2.11 in [B].
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: weitere Beispiele für Signaturen und Strukturen, Eigenschaftern 2-stelliger Relationen, Äquivalenzrelationen, Ordnungen, arithmetische Strukturen, Wörter als Strukturen, relationale Datenbanken als Strukturen; Restriktionen und Expansionen; Isomorphie
Material:
Skript Seiten 107-114
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: 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; die Modellbeziehung
Material:
Skript Seiten 114-128
Weitere Lektüre:
Kapitel III.1 und Kapitel II.1-3 in [EFT].
Weiter mit Kapitel 3: Logik erster Stufe - heute: Subterme, Subformeln und Syntaxbäume; Formulierung und Beweis des Isomorphielemmas der Logik erster Stufe (für Terme und Formeln); generelle Form von Beweisen per Induktion über den Aufbau von Termen und Formeln
Material:
Skript Seiten 129-136
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: 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, Datenbanken
Material:
Skript Seiten 136-147
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: 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; Äquivalenz von Formeln der Logik erster Stufe; relationale Signaturen; Ehrenfeucht-Fraisse-Spiele: Spielregeln des m-Runden EF-Spiels
Material:
Skript Seiten 147-155
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: EF-Spiele: Gewinnbedingung, partielle Isomorphismen, Beispiele; Formalisierung des Begriffs "Gewinnstrategie"; der Begriff der Quantorentiefe einer FO-Formel; Formulierung des Satzes von Ehrenfeucht (ohne Beweis); Erklärung, wie Spoiler durch "Ausspielen einer Formel" eine Gewinnstrategie erhält; Beweis der einfachen Version des Satzes von Ehrenfeucht (Induktionsanfang)
Material:
Skript Seiten 155-163
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 (heute: Induktionsschritt); Begriff der FO-Definierbarkeit einer Klasse von σ-Strukturen, Korollar über nicht-FO-definierbare Klassen von σ-Strukturen; das EF-Spiel auf 2 endlichen linearen Ordnungen; Beweis, dass Duplicator eine Gewinnstrategie im m-Runden EF-Spiel auf 2 endlichen linearen Ordnungen der Kardinalität > 2m besitzt; Folgerung, dass die Klasse aller endlichen linearen Ordnungen gerader Kardinalität nicht FO-definierbar ist
Material:
Skript Seiten 163-169
Weitere Lektüre:
Kapitel 3.2 und 3.3 in [L]
Weiter mit Kapitel 3: Logik erster Stufe - heute: Beweis des Resultats, das besagt, dass weder Graph-Zusammenhang noch Erreichbarkeit FO-definierbar sind; Bemerkung zur Methode der logischen Reduktionen; 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:
Skript Seiten 169-177
Weitere Lektüre:
Kapitel 3.5 und 3.2 und 3.6 in [L];
Kapitel 2.2 in [S]
Abschluss von Kapitel 3: Logik erster Stufe - heute: Beweis, dass jede FO-Formel äquivalent zu einer Formel in Pränex-Normalform ist Start mit Kapitel 4: Grundlagen des automatischen Schließens - heute: Ableitungsregeln, Kalküle, Ableitungen in Kalkülen; 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:
Skript Seiten 177-189
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 und Effektivität der Grundregeln (V) und (E) und der aussagenlogischen Regeln ( (FU), (W), etc ); Substitutionen und das Substitutionslemma (ohne Beweis)
Material:
Skript Seiten 189-197
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: Einführung und Korrektheit und Effektivität der Quantorenregeln "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; 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
Material:
Skript Seiten 197-207
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: der Endlichkeitssatz (inkl. Beweis unter Verwendung des Vollständigkeitssatzes); erststufige Axiomatisierbarkeit; Anwendung des Endlichkeitssatzes zum Beweis der Nicht-Axiomatisierbarkeit der Endlichkeit
Material:
Skript Seiten 207-212
Weitere Lektüre:
Kapitel IV.7, V und VI.1-3 in [EFT]
Weiter mit Kapitel 4: Grundlagen des automatischen Schließens - heute: Anwendung des Endlichkeitssatzes zum Beweis der Nicht-Axiomatisierbarkeit von Graph-Zusammenhang; 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; Beginn des Beweises der Unentscheidbarkeit des Allgemeingültigkeitsproblems für die Logik erster Stufe (durch Nutzen der Unentscheidbarkeit des Postschen Korrespondenzproblems)
Material:
Skript Seiten 212-221
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: Abschluss des Beweises der Unentscheidbarkeit des Allgemeingültigkeitsproblems für die Logik erster Stufe (durch Nutzen der Unentscheidbarkeit des Postschen Korrespondenzproblems); Unentscheidbarkeit des Unerfüllbarkeitsproblems und des Folgerungsproblems und der Nicht-Semi-Entscheidbarkeit des Erfüllbarkeitsproblems für die Logik erster Stufe; Beginn mit Kapitel 4.5 über den Satz von Herbrand: Grundterme, Herbrandstrukturen
Material:
Skript 221-227
Weitere Lektüre:
Kapitel 2.4 in [S] und
Kapitel XI.1-3 in [EFT]
Weiter mit Kapitel 4: Grundlagen des automatischen Schließens - heute: 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:
Skript Seiten
227-233
Weitere Lektüre:
Kapitel 2.4 in [S]
Abschluss von Kapitel 4: Grundlagen des automatischen Schließens
- heute: Skolemisierung, 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,
Material:
Skript 233-243
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: 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 Logik-Programms; viele Beispiele; ein Beispiel zum Unterschied zwischen Theorie und Praxis (Wege in gerichteten Graphen)
Material:
Skript 243-256
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]
weiter mit Kapitel 5: Logik-Programmierung - heute: Anfragen an Logikprogramme; 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); der Unifikationsalgorithmus MGU(t,s) Beispiele zur Anwendung des Algorithmus MGU(t,s)
Material:
Skript 256-270
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: 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); abschließende Bemerkungen zum Unterschied zwischen Beweisbäumen und Suchbäumen und zur Unifikation in Prolog.
Material:
Skript 270-278
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.