Termersetzungssysteme
(V3 resp. 4 + Ü2, SS 2011)
|
|
Für Details und weitere Informationen wird auf die englische Seite zur Vorlesung verwiesen.
Die Vorlesung findet 3-stündig für Studierende der folgenden Studiengänge
statt:
- Master Informatik
- Master Software Systems Engineering
- Master Mathematik
- Bachelor Informatik
- Da es sich um eine "einführende Master-Veranstaltung" handelt, kann sie auch als
Bachelor-Wahlpflichtveranstaltung (Theorie) im Studiengang Bachelor Informatik gehört werden.
- Ebenso ist es möglich, die Vorlesung bereits im Bachelor-Studiengang
zu hören und zu prüfen und sie sich später für den
Master-Studiengang
anerkennen zu lassen.
Die Vorlesung findet 4-stündig für Studierende der folgenden Studiengänge
statt:
- Diplom Informatik
- Diplom Mathematik
Wenden Sie sich bei Fragen bitte an die Sammeladresse tes11@i2.informatik.rwth-aachen.de,
die von den drei Assistenten gelesen wird. Weitere Kontaktdaten finden Sie auf
der Homepage des LuFG I2.
Skript
Das Skript zur Vorlesung ist hier erhältlich: Skript (Fassung vom 4.4.2011)
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
englisch oder 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
Wahlpflichtfach Theorie (für Bachelor),
Theoretische Informatik (für Master),
Theoretische Informatik und Informatik Vertiefung (für Diplom und Master SSE)
Übungen
Studierende in Diplom Studiengängen können den Übungsschein
zur Vorlesung durch Erreichen von 50% der Punkte in den Übungen erlangen.
Den Erwerb eines Übungsscheines empfehlen wir sehr, da dies eine gute
Vorbereitung für die Diplomprüfung darstellt.
Studierende anderer Studiengänge müssen
50% der Punkte in den Übungsblättern erreichen, um an der
Prüfung teilnehmen zu können.
Um am Übungsbetrieb teilnehmen zu können, melden sie sich bitte
hier an.