Logik (Gleichungslogik) (WS 2004/05)

TU München - Fakultät für Informatik
Software- and Systems Engineering Research Group

Vorlesung | Wintersemester 2004/05
Logik (Gleichungslogik)
Prof. Tobias Nipkow

Zeit und Ort:	Fr 13:30 - 15:00, HS 2 (MI 00.04.011)
Beginn:	29. Oktober
Übungsleitung:	Clemens Ballarin

Übungsblätter
1. Übungsblatt [Aufgabe ]	Relationen und Reduktionssysteme
2. Übungsblatt [Aufgabe ]	Terminierung und Ordnungen
3. Übungsblatt [Aufgabe]	Substitutionen, Multimengenordnung
4. Übungsblatt [Aufgabe ]	Terme, Modelle, Gleichungstheorien
5. Übungsblatt [Aufgabe ]	Äquivalenzklassen, Modelle
6. Übungsblatt [Aufgabe ]	Unifikation und Matching
7. Übungsblatt [Aufgabe ]	Terminierung von Termersetzungssystemen, Unifikation
8. Übungsblatt [Aufgabe]	Polynomordnung, Kritische Paare
9. Übungsblatt [Aufgabe ]	Vervollständigung, Lineare Termersetzungssysteme
10. Übungsblatt [Aufgabe ]	Lambda-Kalkül
11. Übungsblatt [Aufgabe ]	Beta-Reduktion
12. Übungsblatt [Aufgabe]	Beta-Reduktion, Normalisierung
13. Übungsblatt [Aufgabe ]	Typsysteme
Programmieraufgaben
6. Übungsblatt [Aufgabe ]	Matching
7. Übungsblatt [Aufgabe ]	Unifikation

Die Lösungen werden Anfang Mai 2005 vom Netz genommen.

Die Klausur zur Vorlesung Gleichungslogik findet, wie bereits angekündigt, am Freitag, den 11. Februar, um 12.45 Uhr statt. Ort ist Hörsaal 2. Wenn Sie an der Klausur teilnehmen möchten, melden Sie sich bitte per E-Mail an ballarin@in.tum.de an, und geben Sie Namen, Matrikelnummer, Fach und Studiengang (Diplom oder Master) an. Anmeldeschluss ist der 31. Januar. Bitte bringen Sie zur Klausur sowohl einen Lichtbild- als auch Ihren Studienausweis mit. Als Hilfsmittel sind zugelassen das Buch Term Rewriting and All That, das Skript Lambda-Kalkül, und eigene Aufzeichungen. Letztere bitte in gebundener Form, es sind keine losen Blätter zugelassen!

Kommentar zu den Hilfsmitteln: Insbesondere nicht zugelassen sind weitere Skripten und die ausgedruckten Musterlösungen. Dagegen können die Übungsblätter zu den Aufzeichnungen dazugeheftet werden. Durch die Bindung muss sichergestellt sein, dass während der Klausur keine Blätter entnommen werden, ohne dass dies auffällt.