Notes on Transformation Orderings Joachim Steinbach Fachbereich Informatik, Universitaet Kaiserslautern Postfach 3049, W-6750 Kaiserslautern, GERMANY E-mail: steinba@informatik.uni-kl.de Abstract An important property and also a crucial point of a term rewriting system is its termination. Transformation orderings, developed by Bellegarde & Lescanne strongly based on a work of Bachmair & Dershowitz, represent a general technique for extending orderings. The main characteristics of this method are two rewriting relations, one for transforming terms and the other for ensuring the well-foundedness of the ordering. The central problem of this approach concerns the choice of the two relations such that the termination of a given term rewriting system can be proved. In this communication, we present a heuristic-based algorithm that partially solves this problem. Furthermore, we show how to simulate well-known orderings on strings by transformation orderings. Keywords Termination of Term Rewriting Systems, Reduction Orderings Source anonymous FTP server ftp.uni-kl.de [131.246.94.94] path: /reports_uni-kl/computer_science/SEKI/1992/papers/ file: Steinbach.SR-92-23.ps.SEKI.Z