Theoretische Informatik und Logik

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

Dozent

Steffen Hölldobler

Tutor

Umfang (SWS)

4/2/0

Module

INF-B-290

Leistungskontrolle

Klausur

Information

Neuigkeiten

Für die nächsten zwei Übungsblätter habt Ihr die Möglichkeit Eure Lösungen bis zum Montag den 23.5. und Montag den 30.5. bis um 14 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.

Am Montag, den 30.05.2016, findet die Vorlesung ausnahmsweise in CHE (Chemie-Hörsaal) 91 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 Freitag, 14 Uhr (in der Woche vor 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 Übungsufgaben 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

Klausur

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