|
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.
Organisatorisches (entlang der Webseite der Vorlesung).
Start mit Kapitel 2: Aussagenlogik - heute: Syntax der
Aussagenlogik.
Material:
Folien,
Skript zu Kapitel 1,
Skript zu Kapitel
2 - Teil 1,
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].
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: Interpretationen, Semantik der Aussagenlogik, rekursive Definitionen über Formeln, Modelle, das Koinzidenzlemma, Wahrheitstafeln, ein Logikrätsel, computerlesbare Darstellung von Formeln, Demo des Formelcheckers für die Aussagenlogik "(tks.AL)", Auflösung des Rätsels zur Geburtstagsfeier (Beispiel 2.1), Erfüllbarkeit, Allgemeingültigkeit, die Folgerungsbeziehung.
Material:
Folien,
Skript zu Kapitel
2 - Teil 2,
Formelchecker für die Aussagenlogik: (tks.AL)
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: die Folgerungsbeziehung; Modus Ponens; Zusammenhänge zwischen Allgemeingültigkeit, Erfüllbarkeit und Folgerungsbeziehung; aussagenlogische Modellierung am Beispiel von Sudokus und automatischer Hardwareverifikation; Äquivalenz von Formeln und Formelmengen; fundamentale Äquivalenzen
Material:
Folien,
Skript zu Kapitel
2 - Teil 3, Ü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: der Dualitätssatz; Beweise per Induktion über den Aufbau von Formeln; boolesche Funktionen und Vollständigkeit der Aussagenlogik; Adäquatheit von Mengen von Junktoren und Konstanten; exklusives Oder, der Mehrheitsjunktor und der Sheffer-Strich; Negationsnormalform (NNF)
Material:
Folien,
Skript zu Kapitel
2 - Teil 4
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: ein Beispiel zur Transformation in NNF; DNF und KNF; eine kleine Formel mit großer DNF; der Endlichkeitssatz
Material:
Folien,
Skript zu Kapitel
2 - Teil 5,
Ü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: Abschluss des 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; Repräsentation von KNF-Formeln durch endliche Klauselmengen
Material:
Folien,
Skript zu Kapitel
2 - Teil 6
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 Begriff einer Resolvente zweier Klauseln; das Resolutionslemma; Resolutionsableitungen und Resolutionswiderlegungen; Korrektheit und Vollständigkeit der Resolution (Beginn des Beweises von Satz 2.61, der besagt, dass eine Klauselmenge genau dann eine Resolutionswiderlegung besitzt, wenn sie unerfüllbar ist)
Material:
Folien,
Skript zu Kapitel
2 - Teil 7,
Ü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: Abschluss des Beweises von Satz 2.61, der besagt, dass eine Klauselmenge genau dann eine Resolutionswiderlegung besitzt, wenn sie unerfüllbar ist; 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:
Folien,
Skript zu Kapitel
2 - Teil 8
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)
Material:
Folien,
Skript zu Kapitel
2 - Teil 8,
Übungsblatt 4
Weitere Lektüre:
Kapitel 3.A und 3.B in [KK],
Kapitel 1.3 in [S],
Kapitel 2.11 in [B].
An Stelle der Vorlesung fand heute eine Fragestunde statt. Es wurden Hinweise zur Lösung des neues Aufgabenblatts gegeben, dazu ähnliche Beispielen besprochen, und es gab die Möglichkeit, Fragen zum Stoff der Vorlesung zu stellen.
Start mit Kapitel 3: Logik-Programmierung - heute: Einführung ins Thema ("deklarativ" vs. "imperativ") und Anwendungsgebiete der Logikprogrammierung; Syntax und Semantik von Logikprogrammen: Fakten, Anfragen, Variablen, Regeln, das Ungleichheitsprädikat, 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,
Skript zu Kapitel
3 - Teil 1,
Quelltext der Programme
bibel1.pl,
party1.pl,
plus1.pl,
plus2.pl,
bibel2.pl,
bibel3.pl,
bibel4.pl,
bibel5.pl
Ein Übungsblatt wurde heute nicht ausgeteilt; das nächste Übungsblatt wird
es nächsten Mittwoch (26.11.) geben.
Weitere Lektüre:
Introduction und Chapter 1 (Basic Constructs) in [SS],
Kapitel 3.C in [KK],
Kapitel 3.1 und 3.2 in [S]
Weiter mit Kapitel 3: Logik-Programmierung - heute: Rekursive Programme und Datentypen, Vorfahren und Nachkommen, Wege in gerichteten Graphen, Unterschied zwischen Theorie und Praxis, natürliche Zahlen in Unärdarstellung, Listen, Quicksort als Logikprogramm, Beispiele für Beweisbäume
Material:
Folien,
Skript zu Kapitel
3 - Teil 2,
Quelltext der Programme
bibel6.pl,
digraph1.pl,
digraph2.pl,
unat1.pl,
listenfkt.pl.
Weitere Lektüre:
Chapter 2 (Database Programming) und Chapter 3 (Recursive Programming) in [SS]
Weiter mit Kapitel 3: Logik-Programmierung - heute: Beispiele für Logik-Programme: binäre Suchbäume, aussagenlogische Formeln, Normalformen für aussagenlogische Formeln; denotationelle vs. operationelle Semantik
Material:
Folien,
Skript zu Kapitel
3 - Teil 3,
Quelltext der Programme
seachtree.pl,
al.pl,
alnormalformen.pl,
Übungsblatt 5
Weitere Lektüre:
Chapter 3 (Recursive Programming) und Chapter 5.1 (Semantics) in [SS]
Weiter mit Kapitel 3: Logik-Programmierung - heute: mehr über Substitutionen, Umbenennungen, ein einfacher Interpreter für Logikprogramme, Satz über die Korrektheit und Vollständigkeit des Interpreters, Beweis der Vollständigkeit, d.h. der Richtung (a)=>(b)
Material:
Folien,
Skript zu Kapitel
3 - Teil 4
Weitere Lektüre:
Chapter 1.8 und Chapter 5.1 und 5.2 in [SS]
Weiter mit Kapitel 3: Logik-Programmierung - heute: Beweis der Korrektheit, d.h. der Richtung (b)=>(a) des Interpreters ANTWORT(Pi,alpha); Unifikation, allgemeinste Unifikatoren (kurz: mgu, für "most general unifier"), Lemma zur Eindeutigkeit von mgus (ohne Beweis) ein Algorithmus zum Finden allgemeinster Unifikatoren; ein Interpreter für Logikprogramme mit allgemeinsten Unifikatoren (der Algorithmus UANTWORT(Pi,alpha)), Satz über die Korrektheit und Vollständikeit des Algorithmus UANTWORT (ohne Beweis); abschließende Bemerkungen zur Implementation des Interpreters in logischen Programmiersprachen
Material:
Folien,
Skript zu Kapitel
3 - Teil 5,
Übungsblatt 6
Weitere Lektüre:
Chapter 4 in [SS]
Abschluss von Kapitel 3: Logik-Programmierung - heute: Prolog: ein Prologinterpreter (der Algorithmus PANTWORT(Pi,alpha)), Vergleich zwischen der deklarativen Semantik und der Prolog-Semantik von Logik-Programmen, Terminierung, Beispiele, Suchbäume, das in Prolog eingebaute Prädikat ! (Cut), Unifikation in Prolog
Material:
Folien,
Skript zu Kapitel
3 - Teil 6,
Quelltext der Programme
bsp1-PAntwort.pl,
myplus1.pl,
myplus2.pl,
myplus3.pl,
cutbsp2.pl
Weitere Lektüre:
Chapter 5.4, Chapter 6 und Chapter 7 in [SS]
Start mit Kapitel 4: Logik erster Stufe - heute: Signaturen, Strukturen, Eigenschaftern 2-stelliger Relationen, Äquivalenzrelationen, Ordnungen, arithmetische Strukturen, Wörter als Strukturen, Transitionssysteme, relationale Datenbanken als Strukturen
Material:
Folien,
Skript zu Kapitel
4 - Teil 1, Übungsblatt 7
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 4: Logik erster Stufe - heute: Strukturen aus Logikprogrammen, Restriktionen und Expansionen, Isomorphie, Variablen, Terme der Logik erster Stufe, Belegungen, Interpretationen, Semantik von Termen, Vergleich zwischen Aussagenlogik und Logik erster Stufe, das Alphabet der Logik erster Stufe
Material:
Folien,
Skript zu Kapitel
4 - Teil 2
Weitere Lektüre:
Kapitel III.1 und Kapitel II.1-3 in [EFT].
Weiter mit Kapitel 4: Logik erster Stufe - heute: Syntax und Semantik der Logik erster Stufe; viele Beispiele; die freien Variablen einer Formel der Logik erster Stufe; die Modellbeziehung
Material:
Folien,
Skript zu Kapitel
4 - Teil 3,
Übungsblatt 8
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 4: Logik erster Stufe - heute: Subformeln, Subterme, Syntaxbäume; Beweise per Induktion über den Aufbau von Termen und Formeln der Logik erster Stufe; das Isomorphielemma
Material:
Folien,
Skript zu Kapitel
4 - Teil 4
Weitere Lektüre:
Kapitel II.3-4 und Kapitel III.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 4: Logik erster Stufe - heute: kurze Wiederholung der bisherigen Themen, freie Variablen, Koinzidenzlemma, 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:
Folien,
Skript zu Kapitel
4 - Teil 5,
Übungsblatt 9
Weitere Lektüre:
Kapitel II.5 und Kapitel III.4 und III.6
in [EFT]
Weiter mit Kapitel 4: Logik erster Stufe - heute: Beispiel für Formeln der Logik erster Stufe in verschiedenen Anwendungsbereichen: Transitionssysteme; Logik und Datenbanken: kurze Wiederholung der Repräsentation einer Kinodatenbank als Struktur über einer geeigneten Signatur; Beispiele für in FO formulierte Anfragen an die Datenbank; 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
Material:
Folien,
Skript zu Kapitel
4 - Teil 6
Weitere Lektüre:
Kapitel 1.1 in [L],
Kapitel 4.3 in [FG]
Weiter mit Kapitel 4: Logik erster Stufe - heute: Äquivalenz von Formeln der Logik erster Stufe; relationale Signaturen; Ehrenfeucht-Fraisse-Spiele: Spielregeln des m-Runden EF-Spiels, Gewinnbedingung, partielle Isomorphismen, Beispiele, Formalisierung des Begriffs "Gewinnstrategie", Formulierung des Satzes von Ehrenfeucht (ohne Beweis), der Begriff der Quantorentiefe einer FO-Formel, Formulierung der einfachen Version des Satzes von Ehrenfeucht (deren Beweis in der nächsten Vorlesung gegeben wird).
Material:
Folien,
Skript zu Kapitel
4 - Teil 7,
Übungsblatt 10
Weitere Lektüre:
Kapitel 3.2 und 3.3 in [L]
Weiter mit Kapitel 4: Logik erster Stufe - heute: Beweis 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 (der Beweis des Korollars wird in der nächsten Vorlesung gegeben)
Material:
Folien,
Skript zu Kapitel
4 - Teil 8
Weitere Lektüre:
Kapitel 3.5 in [L]
Weiter mit Kapitel 4: Logik erster Stufe - heute: Beweis des Korollars ü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; Folgerung, dass die Klasse aller endlichen linearen Ordnungen gerader Kardinalität nicht FO-definierbar ist; Beweisskizze des Resultats, das besagt, dass weder Graph-Zusammenhang noch Erreichbarkeit FO-definierbar sind.
Material:
Folien,
Skript zu Kapitel
4 - Teil 9,
Übungsblatt 11
Weitere Lektüre:
Kapitel 3.2 und 3.6 in
[L]
Abschluss von Kapitel 4: Logik erster Stufe - heute: Beweis des Resultats, das besagt, dass Graph-Zusammenhang nicht FO-definierbar ist; 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:
Folien,
Skript zu Kapitel
4 - Teil 10
Weitere Lektüre:
Kapitel 3.6 in
[L],
Kapitel 2.2 in [S],
Start mit Kapitel 5: 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, Kalkül zur Beschreibung der aus einem Logik-Programm ableitbaren Terme); 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,
Skript zu Kapitel
5 - Teil 1,
Übungsblatt 12
Weitere Lektüre:
Kapitel IV.1 in [EFT],
Weiter mit Kapitel 5: Grundlagen des automatischen Schließens - heute: der Begriff der Korrektheit von Sequenzenregeln; der Sequenzenkalkül kS (bestehend aus Grundregeln, aussagenlogischen Regeln, Quantorenregeln und Gleichheitsregeln); Substitutionen und das Substitutionslemma (ohne Beweis); die Korrektheit des Sequenzenkalküls kS; Beispiele für Ableitungen im Sequenzenkalkül; ein mittels Ableitungen im Sequenzenkalkül kS definierter Begriff der Beweisbarkeit von Formeln aus Formelmengen
Material:
Folien,
Skript zu Kapitel
5 - Teil 2
Weitere Lektüre:
Kapitel IV.2-4, IV.6 und III.8 in [EFT],
Kapitel 2.2 in [S]
Weiter mit Kapitel 5: Grundlagen des automatischen Schließens - heute: Widerspruchsfreie und widerspruchsvolle Formelmengen; der Vollständigkeitssatz und das Erfüllbarkeitslemma; der Endlichkeitssatz; erststufige Axiomatisierbarkeit; Beweis der Nicht-Axiomatisierbarkeit der Endlichkeit und der Nicht-Axiomatisierbarkeit von Graph-Zusammenhang
Material:
Folien,
Skript zu Kapitel
5 - Teil 3
Weitere Lektüre:
Kapitel IV.7, V und VI.2 in [EFT]
Weiter mit Kapitel 5: Grundlagen des automatischen Schließens - heute: der Satz von Löwenheim und Skolem (ohne Beweis); 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,
Skript zu Kapitel
5 - Teil 4
Weitere Lektüre:
Kapitel 2.3 in [S] und
Kapitel VI.1 und X.1-4 in [EFT]
Abschluss von Kapitel 5: Grundlagen des automatischen Schließens - heute: Der Satz von Herbrand - genauer: Grundterme, Herbrandstrukturen, gleichheitsfreie Formeln, Formeln in Skokemform, Herbrand-Expansionen, der Satz von Gödel-Herbrand-Skolem, der Satz von Herbrand, Anwendung des Satzes, Skolemisierung
Material:
Folien,
Skript zu Kapitel
5 - Teil 5
Weitere Lektüre:
Kapitel 2.4 in [S] und
Kapitel XI.1 in [EFT]
Hilfestellungen zur Klausurvorbereitung. Inbes.: Details zum Ablauf der Klausur und Durcharbeiten einiger Beispiel-Aufgaben
Material: Wichtige Hinweise zum Ablauf der Klausur finden Sie hier. Ein Muster für das Deckblatt der Klausur finden Sie hier. Das Layout der Klausur wird in etwa so aussehen wie das Layout der Beispielklausuren, die am Ende des hier erhältlichen Skripts zur Vorlesung "Diskrete Modellierung" (Goethe-Universität Frankfurt am Main) zu finden sind. Beachten Sie dazu aber, dass die Veranstaltung "Logik in der Informatik" der HU Berlin eine ganz andere Schwerpunktsetzung hat als die "Diskrete Modellierung" der Goethe-Univ. Frankfurt (insbes. hat die Klausur "Diskrete Modellierung" eine Dauer von nur 120 Minuten, die Vorlesung richtet sich an Studierende im 1. Semester und hat nur 3 SWS, und das Thema Logik spielt in der Vorlesung "Diskrete Modellierung" eine untergeordnete Rolle, während es in der "Logik in der Informatik" der HU Berlin das zentrale Thema ist).