|
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.
Eröffnungsveranstaltung. Start mit "Kapitel 0: Einleitung" - heute: Einführung ins Thema und ein historischer Überblick. Klärung von Organisatorischem (entlang der Webseite der Vorlesung). Wiederholung von Grundbegriffen und Schreibweisen, die bereits in der Veranstaltung "Logik in der Informatik" behandelt wurden: Strukturen und Syntax der Logik erster Stufe.
Material:
Skript-Fragmente,
Seiten 1-15 (bis inkl. Definition 0.18)
Weitere Lektüre:
Lehrbuch [EFT]: Vorwort und Kapitel I-III.
Viele Beispiele zur Bedeutung der Logik in der Informatik finden
sich in dem 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). Eine
Vorabversion des Artikels finden Sie hier.
Abschluss von "Kapitel 0: Einleitung" - heute:
Weiter in der Wiederholung von Themen die bereits in der Veranstaltung
"Logik in der Informatik" bzw. "Einführung in die formale Logik für IMP" behandelt wurden: Semantik
der Logik erster Stufe, Isomorphielemma, Koinzidenzlemma
neu: Ein präziser Begriff der Substitution (von Variablen durch Terme) in Formeln der Logik erster Stufe
Material:
Skript-Fragmente,
Seiten 15-27
Weitere Lektüre:
Lehrbuch [EFT]: Vorwort und Kapitel I-III und Kapitel IV-V.
Viele Beispiele zur Bedeutung der Logik in der Informatik finden
sich in dem 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). Eine
Vorabversion des Artikels finden Sie hier.
Start mit "Kapitel 1: Der Vollständigkeitssatz" - heute: Wiederholung aus "Logik in der Informatik": abstrakter Begriff eines Kalküls und der Menge der aus einem Kalkül ableitbaren Elemente; Begriffe: Sequenz, Korrektheit einer Sequenz, Sequenzenregeln, Korrektheit einer Sequenzenregel; Wunschliste von Eigenschaften, die der im Folgenden eingeführte Sequenzenkalkül haben soll (Korrektheit, Vollständigkeit, Effektivität); Beginn der Einführung der Regeln des Sequenzenkalküls; hierbei jeweils direkt die Korrektheit und Effektivität der jeweiligen Regeln bewiesen
Material:
Skript-Fragmente,
Seiten 28-31 (bis inkl. Regel (W)) und Seite 33
Weitere Lektüre:
Lehrbuch [EFT]: Kapitel IV-V.
Weiter mit "Kapitel 1: Der Vollständigkeitssatz" - heute: restliche Regeln des Sequenzenkalküls eingeführt und deren Korrektheit und Effektivität nachgewiesen; Beispiele für Ableitungen im Sequenzenkalkül; Begriffsdefinition: Formel φ ist aus Formelmenge Φ im Sequenzenkalkül beweisbar; Formulierung der ersten Aussage des Vollständigkeitssatzes: eine Formel φ ist aus einer Formelmenge Φ im Sequenzenkalkül ableitbar genau dann wenn die Formel φ aus der Formelmenge Φ folgt; Definition des Begriffs ableitbare Regel im Sequenzenkalkül; Formulierung und Beweisidee von Lemma 1.17
Material:
Skript-Fragmente:
Seiten 31-35 (bis inkl. Lemma 1.17)
Weitere Lektüre:
Lehrbuch [EFT]: Kapitel IV-V.
Weiter mit "Kapitel 1: Der Vollständigkeitssatz" - heute: ableitbare Regeln im Sequenzenkalkül; Eigenschaften widerspruchsvoller bzw. widerspruchsfreier Formelmengen; Formulierung des Vollständigkeitssatzes; Beweis des Vollständigkeitssatzes unter Verwendung des Erfüllbarkeitslemmas; Ausblick zum Beweis des Erfüllbarkeitslemmas; Termstruktur und Terminterpretation
Material:
Skript-Fragmente:
Seiten 35-43
Weitere Lektüre:
Lehrbuch [EFT]: Kapitel IV-V.
Weiter mit "Kapitel 1: Der Vollständigkeitssatz" - heute: kurze Wiederholung der bisher eingeführten Definitionen (inkl. der Definitionen "Termstruktur" und "Terminterpretation"); reduzierte Termstruktur und reduzierte Terminterpretation; negationstreue Formelmengen; Formelmengen, die Beispiele enthalten; Formulierung des Satzes von Henkin
Material:
Skript-Fragmente:
Seiten 43-46
Weitere Lektüre:
Lehrbuch [EFT]: Kapitel IV-V.
Weiter mit "Kapitel 1: Der Vollständigkeitssatz" - heute: Beweis des Satzes von Henkin; Beginn des Beweises von Lemma 1.39 (Erweiterung einer widerspruchsfreien Formelmenge zu einer widerspruchsfreien Formelmenge, die Beispiele enthält — für abzählbare Signaturen)
Material:
Skript-Fragmente:
Seiten 46-48 (bis inkl. Induktionsanfang der Behauptung)
Weitere Lektüre:
Lehrbuch [EFT]: Kapitel IV-V.
Weiter mit "Kapitel 1: Der Vollständigkeitssatz" - heute: Abschluss des Beweises von Lemma 1.39; Beweis von Lemma 1.40 (Erweiterung einer widerspruchsfreien Formelmenge zu einer widerspruchsfreien Formelmenge, die negationstreu ist — für abzählbare Signaturen); Beweis des Erfüllbarkeitslemmas und des Vollständigkeitssatzes für abzählbare Signaturen
Material:
Skript-Fragmente:
Seiten 48-51
Weitere Lektüre:
Lehrbuch [EFT]: Kapitel V.
Weiter mit "Kapitel 1: Der Vollständigkeitssatz" - heute: Formulierung von Varianten der Lemmas 1.39 und 1.40, die auch für nicht-abzählbare Signaturen gelten: Lemma 1.39' und Lemma 1.40'; Beweis des Erfüllbarkeitslemmas und des Vollständigkeitssatzes für beliebige Signaturen unter Verwendung des Lemmas 1.39' und 1.40'; Beweis von Lemma 1.39'
Material:
Notizen zu Kapitel 1
(nicht-abzählbare Signaturen) Seiten 1-7 und
Notizen zu Kapitel 1
(Exkurs) Seiten 8-9 (also die ersten beiden Seiten der pdf-Datei)
Weitere Lektüre:
Lehrbuch [EFT]: Kapitel V.
Weiter mit "Kapitel 1: Der Vollständigkeitssatz" - heute: Exkurs: das Auswahlaxiom, der Wohlordnungssatz und das Zornsche Lemma; Beginn des Beweises von Lemma 1.40' (unter Verwendung des Zornschen Lemmas)
Material:
Notizen zu Kapitel 1
(Exkurs) Seiten 8 und 10-18 (also die Seiten 1 und 3-11 der pdf-Datei)
Weitere Lektüre:
Lehrbuch [E]: Kapitel III.7, IV.2 und VIII.
Abschluss von "Kapitel 1: Der Vollständigkeitssatz" - heute: Abschluss des Beweises von Lemma 1.40'.
Beginn mit "Kapitel 2: Der Endlichkeitssatz und die Sätze von Löwenheim und
Skolem" - heute:
der Endlichkeitssatz; Modellklassen und Axiomatisierbarkeit; die Axiomatisierbarkeit der Unendlichkeit;
Begriffe zur Mächtigkeit von Mengen; Beispiele für die Anwendung des
Endlichkeitssatzes: die Nicht-Axiomatisierbarkeit der
Klasse aller endlichen σ-Strukturen und Beweis der Aussage, dass
Formelmengen, die beliebig große endliche Modelle besitzen, auch unendliche
Modelle besitzen;
noch ein Beispiel für die Anwendung des
Endlichkeitssatzes: die Nicht-Axiomatisierbarkeit der
Klasse ZG aller zusammenhängenden (endlichen oder unendlichen) gerichteten
Graphen; der Satz von Löwenheim und Skolem
Material:
Notizen zu Kapitel 1
(Exkurs): Seiten 8 und 17-19 (also die Seiten 1 und 10-12 der pdf-Datei)
und Skript-Fragmente:
Seiten 53-56
Weitere Lektüre:
Lehrbuch [EFT]:
Kapitel V und VI
Weiter mit "Kapitel 2: Der Endlichkeitssatz und die Sätze von Löwenheim und Skolem" - heute: die Nicht-Axiomatisierbarkeit der Überabzählbarkeit; der absteigende Satz von Löwenheim und Skolem; der aufsteigende Satz von Löwenheim und Skolem; der Begriff der elementaren Äquivalenz zweier σ-Strukturen; der Begriff der Theorie einer σ-Struktur; Nichtstandardmodelle der linear geordneten natürlichen Zahlen; Verwendung der Erkenntnisse hierzu zum Beweis, dass es keinen FO-Satz gibt, der von genau denjenigen endlichen linearen Ordnungen erfüllt wird, deren Universum eine gerade Anzahl von Elementen enthält (Beweis von Martin Otto, 2011)
Material:
Skript-Fragmente:
Seiten 57-60
Weitere Lektüre:
Lehrbuch [EFT]:
Kapitel VI