Proseminar Termersetzung im Wintersemester 2000/01
Mittwochs 16:30-18:00, Raum 0.43, Oettingenstraße 67
Betreuer: Dr. Ralph
Matthes (Raum D1.11)
Inhalt
Terme und Termumformungen kennt jede/r schon aus der Schulzeit. Auf
diese Weise wurde in der Mathematik und allen mathematischen Fächern
gerechnet. Immer jedoch dachte man sich dabei Gleichheit "wirklicher
Größen". In diesem Proseminar soll auf die informatische,
d. h., die syntaktische Seite, eingegangen werden, nämlich den
Prozeß der Umformungen. Zum einen, welche
mathematischen Modelle stecken hinter all diesen Systemen von
Rechenregeln? Dies führt zu den Konzepten abstrakter
Reduktionssysteme und eben der Termersetzungssysteme. Zum anderen, was
läßt sich dann auf dieser Abstraktionsebene noch aussagen? Die
eigentlichen Umformungen aus der Schulzeit (und danach) geben ja lediglich
Beispiele ab. In der Tat erweist sich der abstrakte Zugang als sehr
fruchtbar in den Fragen nach der Terminierung solcher Umformungen,
nach der Eindeutigkeit des erzielten Ergebnisses (Konfluenz) und nach dem
Zusammenhang mit der semantischen Sicht von Gleichheit, speziell nach
deren Entscheidbarkeit. Wichtige Begriffe sind Unifikation (d. h.,
das Lösen von Gleichungssystemen, das z. B. zentral ist
für das Verständnis von PROLOG) und die Vervollständigung (das
Gewinnen von Termersetzungsregeln, die ein terminierendes und
konfluentes Termersetzungssystem ergeben).
Vorbesprechung: Mittwoch, 18. Oktober 2000
Vortragsthemen können auch vorab abgesprochen werden (Email an
matthes@informatik.uni-muenchen.de).
(Geplanter) Ablauf
- 18. 10.
- Organisation, Motivation (Kapitel 1 aus Baader/Nipkow)
Teil I: Grundlagen
- 25.10.
- Abstrakte Ersetzungssysteme: Abschnitte 2.1 und 2.2 sowie Lemma
2.7.2 aus Baader/Nipkow (10 Seiten)
- Vortragender: Andrej Trakostanec
- 1.11.
- Feiertag
- 8.11.
- Termersetzungssysteme: Abschnitte 3.1 und 4.2 aus Baader/Nipkow
(11 Seiten)
- Vortragender: Amadou Sow
- 15.11.
- Unifikation: Abschnitte 4.5 und 4.6 sowie Theorem 2.4.2 aus
Baader/Nipkow (8 1/2 Seiten)
- Wegen Krankheit des gedachten Vortragenden wurde nur ein Abriß des
Unifikationsalgorithmus vom Veranstalter gegeben.
- 22.11.
- Abstrakte Terminierung: Abschnitte 2.3 bis 2.5 aus
Baader/Nipkow (10 Seiten)
- Vortragende: Chrystelle Tokam
- 29.11.
- entfällt
- 6.12.
- Terminierungskriterien: Abschnitte 5.1.2, 5.2 und 5.3 ohne
Hilberts 10. Problem und ohne Proposition 5.3.10 aus
Baader/Nipkow (9 Seiten)
- Vortragender: Evgeniy Dekhtyar
- 13.12.
- Simplifikationsordnungen: Eine Auswahl aus Abschnitt 5.4 von
Baader/Nipkow (20 Seiten vor Auswahl)
- Vortragender: Arthur Pichlkostner
- 20.12.
- Lokale Konfluenz: Abschnitt 6.2 mit Übungsaufgaben, aber ohne
ML-Implementierung aus Baader/Nipkow (7 Seiten)
- Vortragender: Boris Lohner
- 10.1.
- entfällt
Teil II: Anwendungen und Erweiterungen
- 17.1.
- Konfluenz: Abschnitt 2.7 ab Definition 2.7.3 und Abschnitt
6.3 aus Baader/Nipkow (10 Seiten)
- Vortragende: Mbuva Mpore
- 24.1.
- Naive Vervollständigung: Abschnitt 7.1 mit Einführung zu Kapitel 7 und
Übungsaufgaben aus Baader/Nipkow (6 1/2 Seiten)
- Vortragender: Oliver Lehnert
- 30.1. (Dienstag) 16 Uhr 00 (!) im Raum Z1.09
- Verallgemeinerte Vervollständigung: Abschnitt 7.2 aus
Baader/Nipkow (7 Seiten)
- Vortragender: Markus Karl
- 31.1. Doppelsitzung
- (1) Korrektheit des Vervollständigungsverfahrens und Huets Algorithmus:
Abschnitte 7.3 und 7.4 aus Baader/Nipkow (11 Seiten)
- Vortragender: Favio Miranda
- (2) Unifikation: Abschnitte 4.5 und 4.6 aus Baader/Nipkow (8
Seiten)
- Vortragender: Ibrahim Said-Issa
- 7.2.
- Modularitätsfragen I: Abschnitte 9.1 und 9.2 aus Baader/Nipkow (6 Seiten)
- Vortragender: Max Hirner
- 14.2. 17 Uhr 00 im Z1.09 (Sondertermin in der vorlesungsfreien
Zeit)
- Modularitätsfragen II: Abschnitt 9.3 aus Baader/Nipkow (4 Seiten)
- Vortragende: Mbuva Mpore
Was nicht behandelt wird aus Baader/Nipkow
- 2.2, 3.2-3.5, 4.3, 4.4, 4.7, 4.8, Teile von 5.4, S.143f, 6.4, 7.5,
8, 9.4, 10, 11
Literatur
Ralph Matthes
Last modified: Wed Feb 14 16:45:02 CET 2001