Instituts-Logo Logik in der Informatik
Prof. Dr. Nicole Schweikardt
Humboldt-Logo

Logbuch zur Vorlesung Logik in der Informatik

Wintersemester 2024/25

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, dem 15.10.24, fand die Eröffnungsvorlesung statt.


  1. Di, 15.10.2024:

    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-16
    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.

  2. Do, 17.10.2024:

    Abschluss von Kapitel 1: Einführung ins Thema "Logik in der Informatik" — heute: Lernziele, Semesterausblick, Literatur
    Start mit Kapitel 2: Aussagenlogik — heute: Einführung und Beispiele, Syntax und Semantik der Aussagenlogik, rekursive Definitionen über Formeln, Modelle, das Koinzidenzlemma, Vereinbarungen und Notationen

    Material: Skript Seiten 17-33 (bis zum Ende von Folie 56)
    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].

  3. Di, 22.10.2024:

    Weiter mit Kapitel 2: Aussagenlogik - heute: 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, Folgerungsbeziehung, Modus Ponens; Zusammenhänge zwischen Allgemeingültigkeit, Erfüllbarkeit und Folgerungsbeziehung

    Material: Skript Seiten 33-46 (bis inkl. Folie 78), 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].

  4. Do, 26.10.2023:

    Weiter mit Kapitel 2: Aussagenlogik - heute: aussagenlogische Modellierung am Beispiel von Sudokus; kurze Info zur aussagenlogischen Modellierung am Beispiel der automatischen Hardwareverifikation (Details hierzu finden sich im Vorlesungsskript); Äquivalenz von Formeln und Formelmengen; fundamentale Äquivalenzen; Definition des Begriffs duale Formel und Formulierung des Dualitätssatzes

    Material: Skript Seiten 47-55 (bis inkl. Folie 91)
    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].

  5. Di, 29.10.2024:

    Weiter mit Kapitel 2: Aussagenlogik - heute: Beweise per Induktion über den Aufbau von Formeln; Beweis des Dualitätssatzes der Aussagenlogik; boolesche Funktionen und die funktionale Vollständigkeit der Aussagenlogik

    Material: Skript Seiten 53-61
    Weitere Lektüre: Kapitel 2.A in [KK], Kapitel 1.2 und 1.4 in [S], Kapitel 2.6 und 2.8 in [B].

  6. Do, 31.10.2024:

    Weiter mit Kapitel 2: Aussagenlogik - heute: Adäquatheit von Mengen von Junktoren und Konstanten; detaillierter Beweis der Adäquatheit von {¬,∨} und von {¬,∧}; Beweisidee für die Adäquatheit von {0, →}; Beweisidee für die Nicht-Adäquatheit von {∨, ∧, →}; weitere Junktoren: exklusives Oder, der Mehrheitsjunktor und der Sheffer-Strich (NAND-Gatter); Beweisidee für die Adäquatheit des Sheffer-Strichs; Negationsnormalform (NNF): Beispiele, ein Algorithmus zur Transformation in NNF, Satz (heute noch ohne Beweis) zur Existenz von äquivalenten Formeln in NNF

    Material: Skript Seiten 61-66 (bis inkl. Folie 107, aber heute noch ohne Beweis von Satz 2.37)
    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].

  7. Di, 05.11.2024:

    Weiter mit Kapitel 2: Aussagenlogik - heute: Beweis von Satz 2.37 (NNF); Disjunktive Normalform (DNF) und Konjunktive Normalform (KNF); Beispiele und Algorithmen zur Transformation in NNF, DNF und KNF; eine kurze Formel in KNF, so dass jede hierzu äquivalente DNF-Formel exponentiell länger ist; Formulierung des Endlichkeitssatzes

    Material: Skript Seiten 64-65 und 66-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].

  8. Do, 07.11.2024:

    Weiter mit Kapitel 2: Aussagenlogik - heute: der Endlichkeitssatz der Aussagenlogik; eine Anwendung des Endlichkeitssatzes (Nachweis, dass ein unendlicher Graph genau dann k-färbbar ist, wenn jeder endliche Subgraph k-färbbar ist)

    Material: Skript Seiten 73-78
    Weitere Lekt.re: Kapitel 2.B in [KK], Kapitel 1.5 in [S], Kapitel 2.10 in [B].

  9. Di, 12.11.2024:

    Weiter mit Kapitel 2: Aussagenlogik - heute: restliche Details zur Anwendung des Endlichkeitssatzes zum Nachweis, 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 (inkl. Beweis); Resolutionsableitungen und Resolutionswiderlegungen; Beispiel für eine Resolutionswiderlegung; Aussage des Satzes über die Korrektheit und Vollständigkeit der Resolution (d.h.: eine Klauselmenge besitzt genau dann eine Resolutionswiderlegung, wenn sie unerfüllbar ist)

    Material: Skript Seiten 78-86
    Weitere Lektüre: Kapitel 2.B in [KK], Kapitel 1.5 in [S], Kapitel 2.10 in [B].

  10. Do, 14.11.2024:

    Weiter mit Kapitel 2: Aussagenlogik - heute: Beweis des Satzes über die Korrektheit und 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

    Material: Skript Seiten 86-93 (bis zum Ende von Folie 143)
    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).

  11. Di, 19.11.2024:

    Weiter mit Kapitel 2: Aussagenlogik - heute: Details zum DPLL-Algorithmus (inkl. Beispiel); Hornklauseln und Hornformeln; der Streichungsalgorithmus: ein effizienter Erfüllbarkeitsalgorithmus für Hornformeln: Algorithmus, ein Beispiel-Lauf, Laufzeitanalyse und Korrektheitsbeweis)

    Material: Skript Seiten 93-101 (bis zum Ende von Teil (a) von Beispiel 2.65)
    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.

  12. Do, 21.11.2024:

    Abschluss von Kapitel 2: Aussagenlogik - heute: ein weiterer Beispiel-Lauf des Streichungsalgorithmus, Laufzeitanalyse und Korrektheitsbeweis
    Start mit Kapitel 3: Logik erster Stufe - heute: Signaturen, Strukturen, Beispiele für Signaturen und Strukturen, Eigenschaften 2-stelliger Relationen, Äquivalenzrelationen, Ordnungen, arithmetische Strukturen

    Material: Skript Seiten 101-110 (bis inkl. Folie 164)
    Weitere Lektüre: Kapitel I und Kapitel III.1 in [EFT].

  13. Di, 26.11.2024:

    Weiter mit Kapitel 3: Logik erster Stufe - heute: weitere Beispiele für Signaturen und Strukturen: Wörter als Strukturen, relationale Datenbanken als Strukturen; Restriktionen und Expansionen; 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; ein Beispiel zur Semantik der Logik erster Stufe

    Material: Skript Seiten 110-124 (bis zum Ende von Folie 196)
    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.

  14. Do, 28.11.2024:

    Weiter mit Kapitel 3: Logik erster Stufe - heute: weitere Beispiele zur Semantik der Logik erster Stufe; formale Definition der Semantik der Logik erster Stufe; die Modellbeziehung; Subformeln, Subterme und Syntaxbäume; generelle Form von Beweisen per Induktion über den Aufbau von Termen und Formeln; Formulierung und Beginn des Beweises des Isomorphielemmas der Logik erster Stufe (heute: Beweis für Terme)

    Material: Skript Seiten 124-133
    Weitere Lektüre: Kapitel III.1 und Kapitel II.1-3 in [EFT].

  15. Di, 03.12.2024:

    Weiter mit Kapitel 3: Logik erster Stufe - heute: Abschluss des Beweises des Isomorphielemmas der Logik erster Stufe (heute: für Formeln); generelle Form von Beweisen per Induktion über den Aufbau von Termen und Formeln; das Koinzidenzlemma der Logik erster Stufe; 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

    Material: Skript Seiten 133-142 (bis inkl. Folie 228)
    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]

  16. Do, 05.12.2024:

    Weiter mit Kapitel 3: Logik erster Stufe - heute: Beispiele für Formeln der Logik erster Stufe in verschiedenen Anwendungsbereichen: Arithmetik; Worte, 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; Äquivalenz von Formeln der Logik erster Stufe

    Material: Skript Seiten 142-152 (bis inkl. Folie 247)
    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]

  17. Di, 10.12.2024:

    Weiter mit Kapitel 3: Logik erster Stufe - heute: Übertragung von aussagenlogischen Äquivalenzen auf Äquivalenz von Formeln der Logik erster Stufe (Lemma 3.43); Zusammenspiel zwischen Quantoren und Negationen; das Ersetzungslemma; Beginn des Abschnitts zum Thema "EF-Spiele": relationale Signaturen; Ehrenfeucht-Fraisse-Spiele: Spielregeln des m-Runden EF-Spiels; Gewinnbedingung, partielle Isomorphismen, viele Beispiele; Formalisierung des Begriffs "Gewinnstrategie"

    Material: Skript Seiten 152-158
    Weitere Lektüre: Kapitel 3.2 und 3.3 in [L], Kapitel 4.3 in [FG]

  18. Do, 12.12.2024:

    Weiter mit Kapitel 3: Logik erster Stufe - heute: 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

    Material: Skript Seiten 159-165
    Weitere Lektüre: Kapitel 3.2, 3.3 und 3.5 in [L]

  19. Di, 17.12.2024:

    Weiter mit Kapitel 3: Logik erster Stufe - heute: 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; Nicht-FO-Definierbarkeit von Graph-Zusammenhang (ohne Beweis) und Erreichbarkeit

    Material: Skript Seiten 165-172
    Weitere Lektüre: Kapitel 3.2, 3.3 und 3.6 in [L]

  20. Di, 07.01.2025:

    Abschluss von 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; 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; ein Beispiel

    Material: Skript Seiten 170-184 (bis zum Ende von Folie 295)
    Weitere Lektüre: Kapitel 3.5 und 3.2 und 3.6 in [L], Kapitel 2.2 in [S]

  21. Do, 09.01.2025:

    Weiter mit Kapitel 4: Grundlagen des automatischen Schließens - heute: weitere Beispiele für Kalküle (zur Definition der syntaktisch korrekten aussagenlogischen Formeln, zur Definition der syntaktisch korrekten σ-Terme, 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; 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)

    Material: Skript Seiten 184-194
    Weitere Lektüre: Kapitel IV.1-4, IV.6 und III.8 in [EFT], Kapitel 2.2 in [S]

  22. Di, 14.01.2025:

    Weiter mit Kapitel 4: Grundlagen des automatischen Schließens - heute: Einführung und Korrektheit und Effektivität der aussagenlogischen Regeln ( (FU), (W), etc ); Substitutionen und das Substitutionslemma (ohne Beweis); Einführung und Korrektheit und Effektivität der Quantorenregeln und der Gleichheitsregeln (G) und (S); Einführung und Korrektheit des Sequenzenkalküls kS

    Material: Skript Seiten 194-201 (bis inkl. Folie 319)
    Weitere Lektüre: Kapitel IV.2-4, IV.6 und III.8 in [EFT], Kapitel 2.2 in [S]

  23. Do, 16.01.2025:

    Weiter mit Kapitel 4: Grundlagen des automatischen Schließens - heute: 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; der Endlichkeitssatz

    Material: Skript Seiten 201-208 (bis inkl. Folie 329)
    Weitere Lektüre: Kapitel IV.7, V und VI.1-3 in [EFT]

  24. Di, 21.01.2025:

    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; Anwendung des Endlichkeitssatzes zum Beweis der Nicht-Axiomatisierbarkeit von Graph-Zusammenhang

    Material: Skript Seiten 207-213
    Weitere Lektüre: Kapitel IV.7, V und VI.1-3 in [EFT]

  25. Do, 23.01.2025:

    Weiter mit Kapitel 4: Grundlagen des automatischen Schließens - heute: 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; die Unentscheidbarkeit des Allgemeingültigkeitsproblems für die Logik erster Stufe (vorerst ohne Beweis);
    Beginn mit Kapitel 4.5 über den Satz von Herbrand: Grundterme, Herbrandstrukturen

    Material: Skript Seiten 213-226 (bis zum Ende von Folie 352)
    Weitere Lektüre: Kapitel VI.1-3 und X.1-4 in [EFT], Kapitel 2.3,2.4 in [S]

  26. Di, 28.01.2025:

    Weiter mit Kapitel 4: Grundlagen des automatischen Schließens - heute: Beispiele für Herbrandstrukturen; 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; Skolemisierung (Begriffsdefinition, ein Beispiel, Beweisidee)

    Material: Skript 226-233 (bis inkl. Folie 360)
    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]

  27. Do, 30.01.2025:

    Abschluss von Kapitel 4: Grundlagen des automatischen Schließens - heute: Beweis von Satz 4.52 (Skolemisierung), Grundlagen von automatischen Theorembeweisern, inkl. Verweis auf ausführliches Beispiel
    Start mit Kapitel 5: Logik-Programmierung - heute: Einführung ins Thema ("deklarativ" vs. "imperativ") und Anwendungsgebiete der Logikprogrammierung; zwei Beispiele

    Material: Skript 233-243 (bis inkl. Folie 371)
    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]

  28. Di, 04.02.2025:

    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; Beispiele; ein Beispiel zum Unterschied zwischen Theorie und Praxis (Wege in gerichteten Graphen)

    Material: Skript 243-256 (bis inkl. Folie 397)
    Weitere Lektüre: Introduction und Teil I (also Chapter 1, 2, 3, 4 und 5) in [SS], Kapitel 3.C in [KK]

  29. Do, 06.02.2025:

    Abschluss von Kapitel 5: Logik-Programmierung - heute: Ableitungen aus Logikprogrammen, 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); 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 256-279
    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]

  30. Di, 11.02.2025:

    Hilfestellungen zur Klausurvorbereitung

    Material: Klausurhinweise inkl. Ablauf, Checkliste für den Tag, sowie Beispielaufgaben

  31. Do, 13.02.2025:

    Nachtrag zu Kapitel 4: Grundlagen des automatischen Schließens - heute: Beweis von Satz 4.40: Unentscheidbarkeit des Allgemeingültigkeitsproblems für FO
    weitere Hilfestellungen zur Klausurvorbereitung. Inbes.: Durcharbeiten einiger weiterer Beispiel-Aufgaben

    Material: Skript 221-224.
    Eine Zusammenstellung wichtiger Informationen sowie die in der Vorlesungsstunde verwendeten Beispielaufgaben finden Sie hier.


Last Modified:   13.02.2025
Nicole Schweikardt