Theoretische Informatik und Logik(SS2016)

Theoretische Informatik und Logik

Lehrveranstaltung mit SWS 4/2/0 (Vorlesung/Übung/Praktikum) in SS 2016

Dozent

• Steffen Hölldobler

Tutor

• Emmanuelle Dietz
• Tobias Philipp

Umfang (SWS)

• 4/2/0

Module

• INF-B-290

Leistungskontrolle

• Klausur

• Information

Neuigkeiten

• Ab jetzt habt Ihr immer die Möglichkeit Eure Lösungen bis montags um 15 Uhr abzugeben (in den Briefkasten zwischen der 2005 und 2006 in APB).

Vorlesung

Die Vorlesung findet montags in der 2. DS in APB/E023 und donnerstags in der 4. DS in HSZ/0004 statt.

Vorlesungsfolien

• Einführung
• Prädikatenlogik erster Stufe (aktualisiert am 9.5.2015, 9:45 Uhr)
• Folien Theoretische Informatik

Übungen

Die Übungen finden erst ab der zweiten Vorlesungswoche statt, d.h. ab der Woche vom 11.4.

Vor jeder Übung habt die Möglichkeit Eure eigenen Lösungen zu den Aufgaben korrigieren zu lassen. Dafür solltet Ihr diese bis spätestens Montag, 15 Uhr (in der Woche der entsprechenden Übungswoche) in den Briefkasten zwischen der 2005 und 2006 (in APB) einwerfen.

• Dienstag, 5.DS in APB/E010
• Mittwoch, 4.DS in APB/E010
• Mittwoch, 5.DS in APB/E001
• Freitag, 2.DS in APB/E008
• Freitag, 5.DS in APB/E007

Aufgaben zur Prädikatenlogik

Lösungen zu fast allen Übungsaufgaben, und weitere Übungsaufgaben finden sich in dem Buch "S. Hölldobler et al.: Logik und Logikprogrammierung, Band II: Aufgaben und Lösungen, Synchron Publishers GmbH, 2011""

4.1 Syntax

• Konstruktion von Teiltermen (Aufgabenstellung), 1. Übungswoche
• Über Nachbarn (Aufgabenstellung), 1. Übungswoche

4.2 Substitutionen

• Substitutionskomposition ist eine Substitution (Aufgabenstellung), 2. Übungswoche
• Eigenschaften von Substitutionen (Aufgabenstellung), 2. Übungswoche

4.3 Semantik

• Beispiele zur Interpretationsanwendung (Aufgabenstellung), 3. Übungswoche
• Verschiedene Interpretationen einer Formel (Aufgabenstellung), 3. Übungswoche
• Existenz einer Herbrand-Interpretation (Aufgabenstellung), 3. Übungswoche

• Knifflige Existenz (Aufgabenstellung), 4. Übungswoche
• Falscher Satz für einelementige Domänen (Aufgabenstellung), 4. Übungswoche
• Formel ohne endliche Modelle (Aufgabenstellung), 4. Übungswoche

4.4 Äquivalenz und Normalform

• Modellverlust beim Skolemisieren (Aufgabenstellung), 5. Übungswoche
• Normalformen (Aufgabenstellung), 5. Übungswoche

4.5 Unifikation

• Unifikationsprobleme I (Aufgabenstellung), 5. Übungswoche
• Unifikationsprobleme II (Aufgabenstellung), 5. Übungswoche

• Vergleichbarkeit von Unifikatoren (Aufgabenstellung), 6. Übungswoche
• Zur Terminierung des Unifikationsalgorithmus (Aufgabenstellung), 6. Übungswoche

4.6 Beweisverfahren

• Resolutionsverfahren (Aufgabenstellung), 7.Übungswoche
• Schrittweiser Resolutionsbeweis (Aufgabenstellung), 7.Übungswoche
• Notwendigkeit der Faktorisierung (Aufgabenstellung), 7. Übungswoche

4.7 Implementierung von Beweisverfahren

4.8 Eigenschaften

• Beispiel für korrespondierendes Herbrand-Modell (Aufgabenstellung), 7. Übungswoche

Aufgaben zur Theoretischen Informatik

I. Berechenbarkeit

• 1. Turingmaschinen (Aufgabenstellung), 8.Übungswoche (aktualisiert am 15.6.2016)

• 2. Rekursive Funktionen (Aufgabenstellung), 9.Übungswoche

• 3. LOPP- und WHILE-Programme (Aufgabenstellung) 10.Übungswoche

Klausur

Alte Klausuren über Prädikatenlogik sind hier zu finden: [1]