Rewriting in Computer Science and Logic (326.118)

Zeit: Di 16.30 - 18.00
Ort: T 1010
Erste Veranstaltung: 6.3.2001

Mathematische Strukturen (wie z.B. Gruppen) oder informatische Strukturen (wie z.B. abstrakte Datentypen) können oft durch Axiome beschreiben werden, welche aus Termgleichungen bestehen. Man möchte nun in solchen Theorien automatisch entscheiden können, ob vermutete Aussagen gültig sind oder nicht. Wir befassen uns mit automatischem Beweisen in Gleichungstheorien und den zugehörigen Fragen von Konvergenz und Termination von Systemen von Termersetzungsregeln. Literaturvorschlag: J. Avenhaus, Reduktionssysteme, Springer-Verlag Berlin Heidelberg New York (1995).