Logik in der Informatik
Prof. Dr. Martin Grohe

Logbuch zur Vorlesung Logik in der Informatik

Di, 19.10.10: Folien 1-32. Paradoxien; Syllogismen; Anwendungen der Logik in der Informatik; Syntax der Aussagenlogik
Do, 21.10.10: Folien 33-59. Semantik der Aussagenlogik; Rekursive Definitionen über Formeln; Koinzidenzlemma; Wahrheitstafeln; Erfüllbarkeit; Allgemeingültigkeit; Folgerungsbeziehung; aussagenlogische Modellierung von Sudoku
Di, 26.10.10: Folien 60-75. Anwendung Schaltkreisverifikation; Äquivalenz; Fundamentale Äquivalenzen; Dualität; funktionale Vollständigkeit (ohne Beweis von Satz 2.27); Adäquatheit
Do, 28.10.10: Folien 74-93. Beweis des Stazes über die funktionale Vollständigkeit; Adäquatheit und neue Junktoren; Negationsnormalform; konjunktive und disjunktive Normalform; Kompaktheitssatz (ohne Beweis)
Di, 2.11.10: Folien 93-99. Beweis des Kompaktheitssatzes; Anwendung auf Färbarkeit unendlicher Graphen; Umwandlung in erfüllbarkeitsäquivalente KNF in Linearzeit
Do, 4.11.10: Folien 100-114. Resolventen; Resolutionslemma; Resolutionswiderlegungen; Korrektheit und Vollständigkeit der Resolution; Komplexität des aussagenlogischen Erfüllbarkeitsproblems; Erfüllbarkeitsalgorithmen, insbesondere DPLL
Di, 9.11.10: Folien 113-130. Beispiel für einen Lauf des DPLL-Algorithmus; Hornformeln; Streichungsalgorithmus; Einführung in die Logikprogrammierung und Prolog; Fakten; Anfragen
Do, 11.11.10: Folien 131-140. Regeln; Beispielprogramme; Terme; Substitutionen; Grundterme; Ableitungen; deklarative Semantik; Rekursion
Di, 16.11.10: Folien 141. Beispiele rekursiver Programme und rekursiver Datentypen: Zusammenhang von Graphen; natürliche Zahlen in Unärkodierung; Listen
Do, 18.11.10: Folien 142-150. Binäre Suchbäume; Aussagenlogik in Prolog implementiert; operationale vs deklarative Semantik; einfacher Interpreter für Logikprogramme
Di, 23.11.10: Folien 150-154. Beweis der Korrektheit des einfachen Interpreters; Unifikation; allgemeinstae Unifikatoren; Unifikationsalgorithmus
Do, 25.11.10: Folien 155-164. Beispiele zum Unifikationsalgorithmus; Interpreter für Logikprogramme mit Unifikation; Interpreter für reines Prolog; nichtterminierende Prologberechnungen; Suchbäume
Di, 30.11.10: Folien 165-184. Cut; Unifikation in Prolog; Symbolmengen; Strukturen; Beispiele von Strukturen
Do, 2.12.10: Folien 185-196. Strukturen aus Logikprogrammen; Restriktionen und Expansionen; Isomorphie; Syntax der Logik der 1. Stufe
Di, 7.12.10: Folien 197-203, 207-208. Freie Variablen; Belegungen und Interpretationen; Semantik der Logik der 1. Stufe; Koinzidenzlemma (ohne Beweis); Beispiele
Do, 9.12.10: Folien 203-213. Beispiele; Beweise per Induktion über den Aufbau von Formeln und Termen; Beweis des Koinzidenzlemmas; Isomorphielemma; die von einer Formel definierte Relation
Di, 14.12.10: Folien 214-230. Die definierte Relation; Erfüllbarkeit; Allgemeingültigkeit; Folgerungsbeziehung; Äquivalenz; Substitutionen; Substitutionslemma
Do, 16.12.10: Folien 231-238. Umbenennen gebundener Variablen; Negationsnormalform; Pränexe Normalform
Di, 4.1.11: Folien 239-243, 245. Wiederholung Logik der 1. Stufe; Ableitungen und Kalküle
Do, 6.1.11: Folien 244, 247-255. Abgeschlossene Mengen in Kalkülen; Sequenzenkalkül für die Logik der ersten Stufe; Korrektheit
Di, 11.1.11: Folien 255-260. Korrektheit des Sequenzenkalküls; Beweisbarkeit; Widerspruchsfreiheit; Vollständigkeitssatz
Do, 13.1.11: Folien 261-267. Kompaktheitssatz; Nichtdefinierbarkeit der endlichen Strukturen; Satz von Löwenheim-Skolem; Nichtdefinierbarkeit der zusammenhängenden Graphen
Di, 18.1.11: Folien 268-272. Erfüllbarkeitsäquivalenz und Erfüllbarkeitsreduktionen; Elimination von freien Variablen; Elimination der Gleichheit
Do, 20.1.11: Folien 273-276. Skolem-Normalform; Klauselnormalform; Beispiele
Di, 25.1.11: Probeklausur
Do, 27.1.11: Folien 277-285. Grundterme und Grundatome; Herbrandstrukturen; Satz von Herbrand; Reduktion des prädikatenlogischen auf das aussagenlogische Erfüllbarkeitsproblem
Do, 3.2.11: Folien 286-297. Beweis des Reduktionssatzes; automatische Theorembeweiser; Prädikatenlogische Resolution; Logikprogrammierung und die Logik der 1.Stufe; Nullestellige Relationen
Di, 8.2.11: Folien 298-309. Übersetzung von Logikprogrammen in die Logik der ersten Stufe; Modelltheoretische Charakterisierung der Semantik von Logikprogrammen; minimale Herbrandmodelle
Do, 10.2.11: Folien 308-321. Minimale Herbrandmodelle; modelltheoretische Sichtweise auf Anfragen; Semi-Entscheidbarkeit des Allgemeingültigkeits und des Folgerungdproblems; Unentscheidbarkeit der Logik der 1.Stufe

Di, 15.2.11: Folie 321. Simulation von Turingmaschinen durch Logikprogramme

Last modified: Mon Feb 21 11:52:22 CET 2011
Martin Grohe