Termination of Rewriting
- More and more, term rewriting systems are applied in computer science aswell as in mathematics. They are based on directed equations which may be used as non-deterministic functional programs. Termination is a key property for computing with termrewriting systems.In this thesis, we deal with different classes of so-called simplification orderings which areable to prove the termination of term rewriting systems. Above all, we focus on the problemof applying these termination methods to examples occurring in practice. We introduce aformalism that allows clear representations of orderings. The power of classical simplifica-tion orderings - namely recursive path orderings, path and decomposition orderings, Knuth-Bendix orderings and polynomial orderings - is improved. Further, we restrict these orderingssuch that they are compatible with underlying AC-theories by extending well-known methodsas well as by developing new techniques. For automatically generating all these orderings,heuristic-based algorithms are given. A comparison of these orderings with respect to theirpowers and their time complexities concludes the theoretical part of this thesis. Finally, notonly a detailed statistical evaluation of examples but also a brief introduction into the designof a software tool representing the integration of the specified approaches is given.
- Termination of Rewriting
Author: | Joachim Steinbach |
---|---|
URN: | urn:nbn:de:bsz:386-kluedo-712 |
Advisor: | Jürgen Avenhaus |
Document Type: | Doctoral Thesis |
Language of publication: | English |
Year of Completion: | 1994 |
Year of first Publication: | 1994 |
Publishing Institution: | Technische Universität Kaiserslautern |
Granting Institution: | Technische Universität Kaiserslautern |
Acceptance Date of the Thesis: | 1994/01/28 |
Date of the Publication (Server): | 2000/04/03 |
Faculties / Organisational entities: | Kaiserslautern - Fachbereich Informatik |
DDC-Cassification: | 0 Allgemeines, Informatik, Informationswissenschaft / 004 Informatik |
Licence (German): | Standard gemäß KLUEDO-Leitlinien vor dem 27.05.2011 |