|
Termersetzungssysteme
(V4 + Ü2, SS 2002)
|
|
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?
Zuordnung
Theoretische Informatik, Informatik Vertiefung
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.
Übungen
Für den Übungsschein müssen 50% der Punkte in den
Übungen erreicht werden und voraussichtlich eine kleine mündliche
Prüfung 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 Zweiergruppen
bearbeitet werden und werden jeweils am Dienstag in der
Vorlesung ausgegeben und am Mittwoch eine Woche darauf vor Beginn der
Übung eingesammelt.
- Blatt 1
ps.gz,
pdf.gz
- Blatt 2
ps.gz,
pdf.gz
Lösungsvorschlag
ps.gz,
pdf.gz
- Blatt 3
ps.gz,
pdf.gz
Lösungsvorschlag
ps.gz,
pdf.gz
- Blatt 4
ps.gz,
pdf.gz
Lösungsvorschlag
ps.gz,
pdf.gz
- Blatt 5
ps.gz,
pdf.gz
Lösungsvorschlag
ps.gz,
pdf.gz
- Blatt 6
ps.gz,
pdf.gz
Lösungsvorschlag
ps.gz,
pdf.gz
- Blatt 7
ps.gz,
pdf.gz
- Blatt 8
ps.gz,
pdf.gz
Lösungsvorschlag
ps.gz,
pdf.gz
- Blatt 9
ps.gz,
pdf.gz
Lösungsvorschlag
ps.gz,
pdf.gz
- Blatt 10
ps.gz,
pdf.gz
Lösungsvorschlag
ps.gz,
pdf.gz
- Blatt 11
ps.gz,
pdf.gz
Lösungsvorschlag
ps.gz,
pdf.gz
- Blatt 12
ps.gz,
pdf.gz
Errata
(9. Juni 2002)
Tool
Tool
von René Thiemann zur automatischen Vervollständigung.
Folien
Hier sind die in den Vorlesungen verwendeten Folien
erhältlich.
- Folie 1 (19.4.02)
ps.gz,
pdf.gz
- Folie 2 (23.4.02)
ps.gz,
pdf.gz
- Folie 3 (26.4.02)
ps.gz,
pdf.gz
- Folie 4 (30.4.02)
ps.gz,
pdf.gz
- Folie 5 (30.4.02)
ps.gz,
pdf.gz
- Folie 6 (03.5.02)
ps.gz,
pdf.gz
- Folie 7 (10.5.02)
ps.gz,
pdf.gz
- Folie 8 (14.5.02)
ps.gz,
pdf.gz
- Folie 9 (17.5.02)
ps.gz,
pdf.gz
- Folie 10 (28.5.02)
ps.gz,
pdf.gz
- Folie 11 (31.5.02)
ps.gz,
pdf.gz
- Folie 12 (31.5.02)
ps.gz,
pdf.gz
- Folie 13 (4.6.02)
ps.gz,
pdf.gz
- Folie 14 (11.6.02)
ps.gz,
pdf.gz
- Folie 15 (14.6.02)
ps.gz,
pdf.gz
- Folie 16 (21.6.02)
ps.gz,
pdf.gz
- Folie 17 (25.6.02)
ps.gz,
pdf.gz
- Folie 18 (28.6.02)
ps.gz,
pdf.gz
- Folie 19 (2.7.02)
ps.gz,
pdf.gz
- Folie 20 (5.7.02)
ps.gz,
pdf.gz
- Folie 21 (9.7.02)
ps.gz,
pdf.gz
- Folie 22 (12.7.02)
ps.gz,
pdf.gz
- Folie 23 (16.7.02)
ps.gz,
pdf.gz
