[Back]

E. Jiresch:
"A Term Rewriting Laboratory with Systematic and Random Generation and Heuristic Test Facilities";
Supervisor: B. Gramlich; Universität Wien (Lehramtsstudium UF Informatik und Informatikmanagement / Psychologie und Philosophie, A-190-884-299), 2008; final examination: 2008-07.

Term rewriting systems (TRSs) are a computational model based on
equational systems with applications in Boolean and ring algebra,
automated theorem proving, functional and logic programming and other
areas. Two fundamentally important properties of TRSs are termination
(is every computation in the system finite?) and confluence (do
different ways of computing still preserve the ability of getting a
common result?). While there are a lot of automated tools trying to
(dis)prove termination of TRSs, hardly any program focuses on
confluence. In addition, there is insufficient automated support for
the (systematic and random) generation of TRSs (with specific
properties). The goal of this Master Thesis is to design and implement
a program that features heuristic tests for important properties of
TRSs and random and systematic generation mechanisms. In this
document, we discuss the functionality and usage of the implemented
program trslab. We also cover the relevant basic theory of term
rewriting, as well as the underlying design concepts of the program
and their advantages and disadvantages.

Termersetzungssysteme (engl.: Term rewriting system, TRS) sind ein auf
Gleichungssystemen basierendes Berechnungsmodell. Sie finden
Anwendungen in Bool'scher und Ring-Algebra, automatischem Beweisen,
funktionaler und logischer Progammierung und anderen Gebieten. Zwei
fundamental wichtige Eigenschaften von TRSs sind Termination (ist jede
Berechnung im System endlich?) und Konfluenz (ist es bei
unterschiedlichen Wegen der Berechnung immer möglich, ein gemeinsames
Ergebnis zu erhalten?). Während es zahlreiche automatisierte Tools zum
Beweisen und Widerlegen von Termination von Termersetzungssystemen
gibt, beschäftigt sich kaum ein Programm mit Konfluenz. Zusätzlich
gibt es nicht genug automatische Unterstützung zur (systematischen und
zufälligen) Generierung von TRSs (mit spezifischen Eigenschaften). Das
Ziel dieser Masterarbeit ist es, ein Programm zu entwerfen und zu
implementieren, das sowohl heuristische Tests für wichtige
Eigenschaften von TRSs als auch Mechanismen zur zufälligen und
systematischen Generierung von TRSs bietet. In diesem Dokument stellen
wir die Funktionalität und den Gebrauch des implementierten Programms
trslab vor. Ebenso beschreiben wir die relevanten theoretischen
Grundlagen von Termersetzung sowie die grundlegenden Designkonzepte
des Programms und deren Vor- und Nachteile.

Term rewriting system, (dis)proving program properties, confluence, termination, random generation of systems