|
Termersetzungssysteme
(V4 + Ü2, WS 2006/07)
|
|
Aktuelles
- Das aktualisierte Skript zur Vorlesung ist im Sekretariat verfügbar.
Inhalt
Termersetzungssysteme dienen zum Rechnen und automatischen Beweisen mit
Gleichungen. Außerdem sind Termersetzungssysteme die
Basis-Programmiersprache, die allen funktionalen Programmiersprachen
zugrunde liegt. Termersetzungssysteme werden daher in vielen Bereichen
wie der automatisierten Programmverifikation, der Spezifikation von
Programmen und der deklarativen Programmierung eingesetzt. In der
Vorlesung werden Verfahren vorgestellt, um folgende Fragestellungen
rechnergestützt zu untersuchen:
- Ist das Resultat eines Programms immer eindeutig (Konfluenz)?
- Hält ein Programm immer nach endlich vielen Schritten an
(Terminierung)?
- Erfüllt ein Programm seine Spezifikation (Korrektheit)?
- Wie kann man ein unvollständiges Programm automatisch
vervollständigen?
Sprache
deutsch
Literatur
- J. Avenhaus. Reduktionssysteme. Springer-Verlag, 1995.
- F. Baader und T. Nipkow: Term Rewriting and All That, Cambridge
University Press, 1998.
- R. Bündgen: Termersetzungssysteme, Vieweg, 1998.
- N. Dershowitz and J.-P. Jouannaud. Rewrite Systems. Handbook of
Theoretical Computer Science, Vol. B, Chapter 6: Formal Methods and
Semantics, J. van Leeuwen (ed.), North-Holland, pp. 243-320, 1990.
- Terese. Term Rewriting Systems. Cambridge University Press, 2003.
-
E. Ohlebusch. Advanced Topic in Term Rewriting. Springer-Verlag, 2002.
Zuordnung
Theoretische Informatik, Informatik Vertiefung
Übungen
Für den Übungsschein müssen 50% der Punkte in den
Übungen erreicht werden und die Scheinklausur am Ende des Semesters muss bestanden
werden.
Den Erwerb eines Übungsscheines empfehlen
wir sehr, da dies eine gute Vorbereitung für die
Diplomprüfung
darstellt. Die Übungsblätter sollen in Zweier- oder Dreiergruppen
bearbeitet werden und werden jeweils vor Beginn der
Übung eingesammelt.
Um am Übungsbetrieb teilnehmen zu können, melden Sie sich bitte hier
elektronisch an.
Bei Fragen zur Korrektur kontaktieren Sie bitte einen der HiWis.
- Blatt 1 ps, pdf
Lösung Blatt 1 ps, pdf
- Blatt 2 ps, pdf Lösung Blatt 2 ps, pdf
- Blatt 3 ps, pdf Lösung Blatt 3 ps, pdf
- Blatt 4 ps, pdf Lösung Blatt 4 ps, pdf
- Blatt 5 ps, pdf Lösung Blatt 5 ps, pdf
- Blatt 6 ps, pdf Lösung Blatt 6 ps, pdf
- Blatt 7 ps, pdf Lösung Blatt 7 ps, pdf
- Blatt 8 ps, pdf Lösung Blatt 8 ps, pdf
- Blatt 9 ps, pdf Lösung Blatt 9 ps, pdf
- Blatt 10 ps, pdf
Lösung Blatt 10 ps, pdf
- Blatt 11 ps, pdf
Lösung Blatt 11 ps, pdf
- Blatt 12 ps, pdf Lösung Blatt 12 ps, pdf
- Blatt 13 ps, pdf
Lösung Blatt 13 ps, pdf,
Vervollständigung
- Blatt 14 ps, pdf
Scheinklausur
Die Scheinklausur findet am Freitag, dem 9. Februar, anstelle der Vorlesung statt.
Zur Vorbereitung gibt es hier eine alte Scheinklausur inklusive
Lösung.
Folien
Hier sind die in den Vorlesungen verwendeten Folien erhältlich.
- Folie 1 (18.10.06) ps,
pdf
- Folie 2 (20.10.06) ps,
pdf
- Folie 3 (25.10.06) ps,
pdf
- Folie 4 (27.10.06) ps,
pdf
- Folie 5 (3.11.06) ps,
pdf
- Folie 6 (8.11.06) ps,
pdf
- Folie 7 (8.11.06) ps,
pdf
- Folie 8 (10.11.06) ps,
pdf
- Folie 9 (15.11.06) ps,
pdf
- Folie 10 (22.11.06) ps,
pdf
- Folie 11 (24.11.06) ps,
pdf
- Folie 12 (24.11.06) ps,
pdf
- Folie 13 (24.11.06) ps,
pdf
- Folie 14 (26.11.06) ps,
pdf
- Folie 15 (6.12.06) ps,
pdf
- Folie 16 (8.12.06) ps,
pdf
- Folie 17 (13.12.06) ps,
pdf
- Folie 18 (13.12.06) ps,
pdf
- Folie 19 (20.12.06) ps,
pdf
- Folie 20 (10.1.07)
ps,
pdf
- Folie 21 (12.1.07)
ps,
pdf
- Folie 22 (17.1.06)
ps,
pdf
- Folie 23 (19.1.06)
ps,
pdf
- Folie 24 (19.1.06)
ps,
pdf
- Folie 25 (26.1.06)
ps,
pdf
- Folie 26 (2.2.07)
ps,
pdf
- Folie 27 (7.2.07)
ps,
pdf
- Folie 28 (7.2.07)
ps,
pdf
