|
Term Rewriting Systems
(V4 + Ü2, SS 2004)
|
|
Contents
Term rewriting systems are used for computations and mechanized proofs with
equations. All functional programming languages are based on term
rewriting systems, too. Therefore, term rewriting systems are used
in many areas like mechanized program verification, specification
of programs and declarative programming. The following questions
will be discussed in the course.
- Is the result of a computation always unique (confluence)?
- Does a computation always stop after a finite number of steps (termination)?
- Does a program fulfill its specification (correctness)?
- How can the completion of an incomplete program be handled automatically?
Language
The course is given in German.
References
- 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.
Area
Theoretical Computer Science, Area of Specialization
