About Changing the Ordering during Knuth-Bendix Completion Andrea Sattler-Klein Fachbereich Informatik, Universitaet Kaiserslautern D-67653 Kaiserslautern, GERMANY E-mail: sattler@informatik.uni-kl.de Abstract We will answer a question posed in [DJK91] and will show that Huet's completion algorithm [Hu81] becomes incomplete, i.e. it may generate a term rewriting system that is not confluent, if it is modified in a way that the reduction ordering used for completion can be changed during completion provided that the new ordering is compatible with the actual rules. In particular, we will show that this problem may not only arise if the modified completion algorithm does not terminate: Even if the algorithm terminates without failure, then the generated finite noetherian term rewriting system may be non- confluent. Most existing implementations of the Knuth-Bendix algorithm provide the user with help in choosing a reduction ordering: If an unorientable equation is encountered, then the user has many options, especially, the one to orient the equation manually. The integration of this feature is based on the widespread assumption that, if equations are oriented by hand during completion and the completion process terminates with success, then the generated finite system is a maybe non- terminating but locally confluent system (see e.g. [KZ89]). Our examples will show that this assumption is not true. References [DJK91] N. Dershowitz, J.-P. Jouannaud, J.W. Klop. Open Problems in Rewriting. Proc. Fourth International Conference on Rewriting Techniques and Applications, Como, Italy, Lecture Notes in Computer Science 488 (Springer, Berlin, 1991), 445-456. [Hu81] G. Huet. A complete proof of correctness of the Knuth- Bendix completion algorithm. Journal Computer and System Science 23(1) (1981), 11-21. [KZ89] D. Kapur, H. Zhang. RRL: Rewrite Rule Laboratory - User's Manual. GE Corporate Research and Development Report, Schenectady, New York, 1987 (revised version: May 1989). Keywords Knuth-Bendix completion, term rewriting systems, string rewriting systems Source anonymous FTP server ftp.uni-kl.de [131.246.94.94] path: /reports_uni-kl/computer_science/SEKI/1993/papers/ file: Sattler.SR-93-19.ps.Z